首页 . 理学 . 计算机科学技术 . 计算机科学理论 . 程序设计理论 . 类型理论

程序规约

/program specification/
条目作者卜磊

卜磊

最后更新 2024-12-03
浏览 119
最后更新 2024-12-03
浏览 119
0 意见反馈 条目引用

一种对程序预期行为的定义与描述。

英文名称
program specification
所属学科
计算机科学技术

在软件开发、设计及质量保障中,程序规约发挥了重要作用。

一个良好定义的形式化程序规约会用数学化语言对相关程序活动中所涉及的各类资源、服务、特别是功能等需求进行精确、无二义性的描述。一般情况下,其由程序前置条件与后置条件等几部分组成。所谓前置条件,即程序执行前系统状态满足的条件,而后置条件则描述的是程序执行后系统状态满足的条件。换句话说,规约描述了程序执行后,其系统状态会发生什么变化,但是并不描述相关变化如何实现。

基于相关规约,程序设计及开发人员可以对其所面临的问题有一个清晰、准确并一致的认识,从而可以进行有效、准确的设计与实现,保证其实现的程序符合相关规约的要求。特别是在多组件系统的开发和设计中,对各组件行为的精确程序规约会极大地便利各组件开发者之间的沟通、理解,并较大程度避免后续可能出现的不一致性、重复开发等常见问题。

在此之外,程序规约也可以成为程序开发者与程序使用者之间的一份契约(contract),程序开发者基于规约进行设计开发,而使用者则可将规约视作一份用户手册进行使用。一般用户可以基于规约理解程序功能,而程序测试、验证人员则可以基于规约去设计测试用例对程序正确性进行测试,或者采用定理证明或模型检验的方式去验证程序实现方式是否一定满足相关规约的要求,从而保障系统正确性。当然,在规约本身层面,即已可以去进行一致性检查,以防各组件规约间已经出现不一致或者冲突的情况,从而可以提早发现并修复问题。

上述讨论集中在形式化程序规约范畴内。事实上,程序规约也可以是非形式化的,并且在实际软件开发中,因资金、时间等成本所限,非形式化程序规约更为常见。所谓非形式化,即相关规约是采用自然语言来描述。其优点是便于表达,易于普通程序开发者进行交互与理解;其缺点在于,由于自然语言的二义性,可能存在理解不一致等情况的存在,从而导致后续问题。

相关条目

阅读历史

    意见反馈

    提 交

    感谢您的反馈

    我们会尽快处理您的反馈!
    您可以进入个人中心的反馈栏目查看反馈详情。
    谢谢!