标签：语言 作业 面向对象 规格 操作符 单元 JML 前置条件 表达式

一、梳理JML语言的理论基础、应用工具链情况

JML的语言基础主要包括JML表达式、方法规格以及类规格

1、JML表达式

（1）原子表达式

　　\result

　　\old()

　　\not_assigned()

　　\not_modified()

　　\nonnullelements()

　　\type()

　　\typeof()

（2）量化表达式

　　\forall

　　\exists

　　\sum

　　\product

　　\max

　　\min

　　\num_of

（3）操作符

　　子类型关系操作符  <:

　　等价关系操作符  <==>

　　推理操作符  ==>

　　变量应用  \nothing  \everything

2、方法规格

（1）前置条件  reqquires

（2）后置条件  ensures

（3）副作用范围限定  assignable  modifiable

（4）signals子句

3、类规格

（1）状态变化约束  constraint

（2）不变式  invariant

　　

标签：语言,作业,面向对象,规格,操作符,单元,JML,前置条件,表达式
来源： https://www.cnblogs.com/xcb990105/p/10898743.html

本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享；
2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关；
3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关；
4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除；
5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。