CMurphi入门笔记(四)——表达式
发布日期:2022-02-22 16:04:56 浏览次数:13 分类:技术文章

本文共 1649 字,大约阅读时间需要 5 分钟。

原文地址:

 

类型是根据名称区分的。任何整数子区间类型的表达式都是合法的,一个整数表达式也是合法的(虽然这样做可能会导致运行时错误)。布尔类型和整数表达式是不兼容的。

上边的第二句话原文为:Expressions of any integer subrange type
are legal wherever an integer expression is legal

在变量初始化之前使用变量是错误的,这个错误会在运行时检测。所有的运行时错误都是由验证器检测的。

越界使用数组也是错误的,同样,这个错误也是在运行时检测。

下边对表达式的语法进行说明。

指示符

     
       ::=
      
 { .   | \[   \] }

通常,"<designator>.<ID>"的形式代表选择记录中的一个域,而"<designator>[<expr>]"的形式代表选择数组中的一个元素。

表达式

     
       ::=  \( expr \)
      
 | 
 | 
 |   \(   \)
   -- a function call.
 | forall 
do   endforall
-- universal quantification.
 | exists 
   do   endexists
-- existential quantification.
 |   + 
 |   - 
 |   * 
-- multiplication.
 |   / 
-- integer division.
 |   % 
-- remainder.
 | ! 
   -- logical negation.
 |   | 
-- logical disjunction.
 |   & 
-- logical conjunction.
 |   -> 
   -- logical implication.
 |   < 
 |   <= 
 |   > 
 |   >= 
 |   = 
 |   != 
 |   ?   : 
-- C-style conditional expression.

其中运算符有:

?:
->
|
 &
!
< <= = != >= >
 + -
* / %

上边运算符的优先级是按照从低到高排序的,同一行的运算符具有相同的优先级。

  • "+","-","*","/","%","<","<=",">=",">"仅仅为整数运算定义。
  • "="和"!="仅仅为简单运算定义。
  • "&","|","!",和"->"仅仅为布尔运算定义。
  • 对于"?:"运算符,测试条件必须是布尔表达式,两个候选者必须是类型兼容的。
  • "+","-","*","/",和"%"返回整数,其他均返回布尔类型,除"?:"之外。

"Forall"和"Exists"运算符

以后我们会对这两个进行更加详细的介绍。现在对量词表达式(即使用了"forall"或者"exists"的表达式)中使用的<quantifier>进行说明。对于量词表达式,其子表达式必须是一个布尔表达式,它将对quantifier中的每一个值进行测试。"forall"表达式在其quantifier中的每一个值测试均为true的时候为true,"exists"表达式在其quantifier中的某些值测试为true的时候就为true。


 

表达式这一部分大家还是很熟悉的吧~也比较容易理解~

 

传送门:

 

 

 

转载于:https://www.cnblogs.com/Rainday/p/cmurphi_prime_4.html

转载地址:https://blog.csdn.net/dianchoucong6518/article/details/102293624 如侵犯您的版权,请留言回复原文章的地址,我们会给您删除此文章,给您带来不便请您谅解!

上一篇:CMurphi入门笔记(三)——定义
下一篇:CMurphi入门笔记(六)——规则,起始状态和不变式

发表评论

最新留言

不错!
[***.191.171.22]2022年10月17日 20时43分47秒

关于作者

    喝酒易醉,品茶养心,人生如梦,品茶悟道,何以解忧?唯有杜康!
-- 愿君每日到此一游!

最新文章

ArrayList和LinkedList的底层原码分析 2019-12-25 02:37:26
AspectJ切入点@Pointcut语法详解非常详细(附接口请求详情打印代码demo) 2019-12-25 02:37:24
项目性能遇到瓶颈,需要分库分表,主键id如何处理? 2019-12-25 02:37:24
**生信自学记录1——获取Fastq格式的反向互补序列** 2019-12-25 02:37:24
springboot搭建 2019-12-25 02:37:25
azkaban:Failed to find write-enabled DB connection. Wait 15 seconds and retry. 2019-12-25 02:37:23
Phonix:org.apache.hadoop.ipc.RemoteException(org.apache.hadoop.fs.PathIsNotEmptyDirectoryException) 2019-12-25 02:37:23
基于Keil_uVision5中的STM32F103C8编程(一)简易流水灯的实现及拓展 2019-12-25 02:37:23
CentOS下配置java环境 2019-12-25 02:37:23
CentOS下配置Python环境 2019-12-25 02:37:23
Linux下安装mysql 2019-12-25 02:37:23
Linux终端下mysql创建用户、数据库和数据库表 2019-12-25 02:37:24
复制文件夹到集群所有节点的相同目录下的shell脚本 2019-12-25 02:37:22
为何hadoop集群只有一个datanode呢? 2019-12-25 02:37:22
Maven在idea中加载依赖包不成功,或者pom.xml一直报错,如何解决? 2019-12-25 02:37:22
hadoop MR的一些迷糊知识总结 2019-12-25 02:37:22
hadoop 出现bug:Exception in thread “main“ java.lang.UnsatisfiedLinkError 2019-12-25 02:37:22
hive的时间函数 2019-12-25 02:37:22
hive学习笔记(纯手工) 2019-12-25 02:37:22
【IDEA2019.3版本】AJAX请求报错404:URL设置与Servlet映射不一致所致 2019-12-25 02:37:20