程序规约

程序规约（program specification），理学-计算机科学技术-计算机科学理论-程序设计理论-类型理论，一种对程序预期行为的定义与描述。在软件开发、设计及质量保障中，程序规约发挥了重要作用。一个良好定义的形式化程序规约会用数学化语言对相关程序活动中所涉及的各类资源、服务、特别是功能等需求进行精确、无二义性的描述。一般情况下，其由程序前置条件与后置条件等几部分组成。所谓前置条件，即程序执行前系统状态满足的条件，而后置条件则描述的是程序执行后系统状态满足的条件。换句话说，规约描述了程序执行后，其系统状态会发生什么变化，但是并不描述相关变化如何实现。基于相关规约，程序设计及开发人员可以对其所面临的问题有一个清晰、准确并一致的认识，从而可以进行有效、准确的设计与实现，保证其实现的程序符合相关规约的要求。特别是在多组件系统的开发和设计中，对各组件行为的精确程序规约会极大地便利各组件开发者之间的沟通、理解，并较大程度避免后续可能出现的不一致性、重复开发等常见问题。