CMurphi入门笔记(六)——规则,起始状态和不变式
发布日期:2022-02-22 16:04:56 浏览次数:15 分类:技术文章

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

原文地址:

 

规则,状态和不变式的语法如下所示:

     
       ::= 
      
        {; 
       
         } [;]
        
 ::= 
 | 
 | 
 | 
 | 

简单规则<simplerule>

     
       ::= rule [
      
       ]
       
   [   ==> ]
   [ {   } begin ]
   [ stmts ]
 end

简单规则决定了非确定性有穷自动机从一个状态到另一个状态的转变。

简单规则描述了状态之间的转变。逻辑上,它由一个块和一个条件组成,其块是将要执行的语句的集合,其条件是一个布尔表达式,描述可能被执行的块下的状态。如果一个状态的条件为true,则该规则的块会被执行来提供到另一个状态的转变。

规则的条件是可选的。如果没有说明条件,则规则被假定为总是可用的。

在规则的条件中使用具有副作用的表达式是错误的。

规则可能定义局部变量,常量或者类型,这些并不是状态的一部分。如果没有定义变量,用来开始块的begin语句可以省略掉。不幸的是,如果既没有条件也没有局部变量,语法分析器常会错误地分析输入。所以,没有条件的规则应该使用保留字begin来开始它的块

一个有条件的规则可以通过下边的转换方法等价地写为一个没有条件的规则:

rule
   rule
  

==>
begin
  
-->
 if 
begin
  
  
 end
end
end

虽然这是功能冗余的,有条件可以使得验证器的速度快3~4倍。

程序中不存在至少一个简单规则是错误的。

起始状态<startstate>

     
       ::= startstate [ 
      
        ]
       
   [ {   } begin ]
   [   ]
 end

起始状态是一条特殊类型的规则。它仅仅在每次运行的开始的时候执行。换句话说,就是每次运行都会执行一个起始状态,然后执行零个或者多个简单规则。

起始状态必须为每一个全局变量赋值,否则将会引发运行时错误。

程序没有至少一个起始状态是错误的。

不变式<invariant>

     
       ::= invariant [ 
      
        ] 
       
      
     

下边的两种形式是等价的:

invariant "foo"
  
rule
 !    ==>
 Error "Invariant violated: foo"   end

某些时候,很多程序猿觉得使用内嵌的"assert"和"error"这种说明风格的语句比使用不变式要更加自然。然后,对于能够方便表达为不变式的特性,表达为不变式要更加有效率,因为编译器可以根据不变式的一些约束特性进行优化。

在不变式中使用具有副作用的表达式是错误的。

规则集<ruleset>:

     
       ::= ruleset 
      
        {; 
       
         }
        
   do
 [ ] end

规则集可以被认为是为其<quantifier>中的每一个值创建一份其<rules>组件的副本。

别名规则<aliasrule>:

 
     
       ::= alias 
      
        {; 
       
         } do [
        
         ] end
        
       
      
     

别名规则创建可以在其所有<rules>组件中使用的规则的别名。

 


CMurphi的基本知识就到这里啦~~

 

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

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

上一篇:CMurphi入门笔记(四)——表达式
下一篇:Could not load file or assembly 'System.Web.Helpers...错误

发表评论

最新留言

哈哈,博客排版真的漂亮呢~
[***.191.171.6]2022年10月07日 01时42分20秒

关于作者

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

最新文章