没有合适的资源?快使用搜索试试~ 我知道了~
理论计算机科学电子札记91(2004)21-42www.elsevier.com/locate/entcs形式化一般正确性杰瑞米·E道森1,2NICTA、RSISE、澳大利亚国立大学,堪培拉ACT 0200,澳大利亚摘要我们考虑邓恩的抽象命令语言,以及他对一般正确性的解释。我们提供了一个操作解释他的抽象命令,并使用自动定理证明系统伊莎贝尔证明,这种操作解释导致邓恩的语义。我们认为,在精确的形式化的文献中发现的一些公式的困难。保留字: 一般的正确性抽象的命令1介绍一般正确性是Jacobs &Gries(1985)[5]作为部分正确性和完全正确性的替代品而引入的,参见Nelson(1989)[8]。Jacobs Gries使用关系模型,将程序表示为初始状态和最终状态之间的关系:它们的最终状态空间包括表示非终止性的“n”。通过这种方式,他们可以区分程序何时保证终止、保证不终止或两者都不保证。部分正确性和完全正确性(单独)都不能做到这一点。在[1]和[2]中,Dunne给出了一般正确性的说明,其中他给出了一组“抽象命令”,以及相关的语义。对于每一个ab-obtain命令,Dunne给出了它的语义,包括它的终止条件、它的最弱自由前提谓词和它的框架,这是(松散的)1 由澳大利亚研究委员会大型赠款2网址:jeremy@csl.anu.edu.au,http://csl.anu.edu.au/~jeremy/1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi:10.1016/j.entcs.2003.12.00422J.E. Dawson / Electronic Notes in Theoretical Computer Science 91(2004)21-可以被命令改变的程序变量的集合。从这些可以得出总,部分和一般的正确性语义。我们描述的抽象命令的操作解释类似的雅各布斯格里斯。然后,我们使用自动证明伊莎贝尔表明,这种解释意味着邓恩给出的语义我们还使用Isabelle来证明他的一些更困难的结果。自动定理证明器的使用有助于确保精确细节的正确陈述,否则这些细节很容易被忽略,并迫使我们解决程序变量和逻辑变量之间的区别(在非正式处理中很容易我们参考Isabelle中证明的结果在[3]中,Gordon提供了程序(命令)的操作解释,并使用HOL定理证明器来验证Hoare逻辑的公理(规则)。他详细解释了这种工作的某些有问题的方面,我们将提到brie brilliy。在[4]中,哈里森在HOL定理证明器中形式化了Dijkstra在[6]中,Lermer和Fidge Hayes考虑了程序表达式的语义他们考虑最弱的自由前提条件,也讨论最强的后置条件。它们的条件比Dunne和本文中讨论的条件更复杂,因为它们考虑了类型化的局部变量和在“上下文”中执行命令2命令和条件命令典型地,人们将命令(或程序)建模为作用于机器状态的函数一个必须终止的确定性命令可以被建模为一个函数,它只返回一个新的机器状态。一个确定性的命令,可能会或可能不会终止可以建模为一个函数,返回一个新的状态或什么都没有,代表的想法,一个非终止命令返回没有结果。然而,如果我们将非确定性程序表示为返回一组新状态的函数,那么这使得我们无法将非终止性表示为几种可能结果之一我们还想表示不可行的命令。(这些是有用的构建块,即使你事实上,这不是非终止,而是自然地由不返回新状态的命令表示。解决方案(Plotkin [9],也被Harrison [4]使用)是考虑命令J.E. Dawson / Electronic Notes in Theoretical Computer Science 91(2004)21-23结果,其中结果是在新状态中终止或非终止。条件布尔表达式,或条件,对机器状态,发生在工作,如在两个上下文中。首先,许多命令(如状态通常表示为从变量名集合到其值的函数。这样一个命令中的条件将最自然地表示为编程语言中的文本,或者抽象语法树,但是由于它能够在任何机器状态中被评估,我们可以很好地将其视为state→bool类型的函数(并且我们可以将state的概念视为抽象实体)。其次,条件Q可以出现在表达式wlp(C,Q)(其中wlp表示最弱自由前提)或{P}C{Q}(Hoare逻辑)中。 最自然的做法可能是将它们视为状态上的谓词(或state→bool类型的函数)。然而,wlp的规则以及Hoare逻辑中的一个相关规则是wlp(x:=E,Q)=Q[x:=E]{Q[x:=E]}(x:=E){Q}我们用Q[x:=E]表示Q,其中x的出现被E取代;其他许多作者将其写成Q[x/E],Q[E/x],QE→x,Q<$E/x<$,{E/x}Q,令人困惑的是,前两个都很流行。当Q是状态的任意谓词时,这些规则中的替换概念就没有意义了;它们要求Q是用命令语言写的表达式,或者类似的东西,或者是一个抽象语法树,包含字面上的程序变量名。请注意,这种谓词的语言必须不能表达一个概念,例如然而,Q也可以包含逻辑变量,如以下霍尔逻辑示例(取自Gordon[3,§5.0],其中X,Y,Z表示程序变量,x,y表示逻辑变量){X=x<$Y=y}(Z:=X;X:=Y;Y:=Z){X=y<$Y=x}在这一点上还值得注意的是,在抽象命令中使用布尔表达式(例如保护命令P→A和预处理命令P|A)布尔值P不被视为片段 而是作为状态的任意谓词。因此,从邓恩对这些命令的处理中可以清楚地看出”[3]这一问题得到了解决。这对我们来说意味着,我们对许多命令(不包括赋值)的分析可以在24J.E. Dawson / Electronic Notes in Theoretical Computer Science 91(2004)21-抽象的层次,其中布尔表达式被建模为状态的谓词,命令被建模为从状态到结果集的函数。下一节将在这一层面进行分析帧邓恩还定义了每个抽象命令都有一个框架。这是一组“可能”被排除的变量。然而,请注意,帧(x:=x)={x}。此外,从任何命令可以定义一个新的命令,它具有一个扩大的框架,但在其他方面是相同的。说明一个命令的框架并不有助于描述该命令的功能,因此我们可以展示,例如,两个命令的行为方式相同,而不考虑它们的框架。本节的工作在此基础上进行请注意,结果因此受到限制,即如果两个抽象命令的框架不同,则它们实际上是不同的。我们认为关于框架的相关证明是非常简单的。文字命令和表达式、命令的框架和赋值命令的考虑将推迟到下一节。3作为状态3.1一元类型如前所述,我们将命令建模为从状态到结果集的函数。这里是类型结果的正式定义。数据类型结果=非术语|Term状态因此,当我们对两个命令A和B的排序进行建模时,我们首先将A应用于给定的状态,获得一组结果,然后我们必须将B应用于从A获得的结果集,B是一个state→outcome set类型的函数。我们可以把这看作当这可以以满足某些条件的方式完成时,我们称类型之间的关系为“单子”。参见Wadler [10]以获得关于单子的更多信息实际上,这是一个复合单子的例子。类型outcome,相对于类型state,是一个单子,其中类型(state→outcome)→(outcome→outcome)的扩展函数将由下式给出:extofNonTerm=NonTermextof(Terms)=fs类型构造函数集合,它对任何类型α给出类型α集合(类型α的事物集合的类型),也给出一个单子,它的扩张函数,J.E. Dawson / Electronic Notes in Theoretical Computer Science 91(2004)21-25类型(α→α集)→(α集→α集),由下式给出外部操作系统=f oo∈ os除了扩展函数之外,monad的指定还包括一个单位函数,它通常以一种相当自然的方式将“基”类型的值转换对于上面提到的两个单子,我们有unito:state→outcome units:α→αsetunitos=Termsunitse={e}还要注意的是,扩展函数通常被称为bind,并以fix格式编写(如[10]),所以extfs=s bindf。两个单子一般不能组成另一个单子,但是上面提到的第一个单子一般可以与任何其他单子组合,得到一个复合单子(见[7,§7.3])。下面给出了扩张函数的公式,包括一般的(单位和外延)和我们对单位和外延的特定选择。在特定情况下,extos的类型为(状态→结果集)→(结果集→结果集)。extosfos=设fJ(Terms)=f sfJNonTerm=单位NonTermextosfos=设fJ(Terms)=f sfJNonTerm={NonTerm}inextsf jos在o∈os中fJo如上所述,monad包括函数unit和ext(适当类型),它们必须满足某些条件,如下所示:extkunit=k(左单位)ext unit=id(右单位)ext(exthk)=exthextk(Ask)令seqAB表示命令A和B的顺序(其中A、B和seqA B的类型为状态→结果集)。 如前所述,我们首先要将A应用于给定的状态,获得一组结果;然后我们必须将B的扩展(类型为结果集→结果集)应用于该结果集。也就是说,seqA B=extosB<$A。然后我们可以证明seq的结合性:seqA(seqB C)=extos(seqB C)=extos(extosCB)A=extosCextosBA通过单子规则(Asn)=extosCseqA B26J.E. Dawson / Electronic Notes in Theoretical Computer Science 91(2004)21-=seq(seqA B)C这在Isabelle中被证明为seq_asq。Dunne [1,§7]使用复合单子的状态→结果集类型的单位函数由下式给出:unitoss=units(Terms)={Terms}这表示命令skip,它总是在初始状态终止3.2细化由于我们通常只给出Isabelle代码,所以我们提到一些不太明显的Isabelle符号。那“怎么样?“表示一个变量,任何东西(合适的类型)都可以替代它。布尔值的逻辑等价性用等价符号=或==表示。按照本文的惯例,我们证明为定理的结果是用引号(通常在定理的名称之前)给出的,而定义是不带一些集合和函数符号(数学和Isabelle等价)如下:a/∈ b∈C Da ~:UNb:C. D{a}(CD)EF\Ginsert a(CUnD)= E Int F- Gλx.E(%x. (E)A→B(蕴涵)A ==> B或A --> B我们定义对应于[1,§2]的wlp,trm和wp的函数。wlpm?C?P?状态==所有状态术语:?C?状态-->?真的吗C?state== NonTerm ~:?C?状态wpm?C?P == wlpm?C?真的?C这里&&和||提升状态上的合取和析取,并且->是谓词之间的“更强” 关系,因此,其中P和Q是状态上的谓词,?P--->?Q ==所有s。什么?P s-->?Q s(?P&&?Q)?s==?P?s&?Q?S(?P||什么?Q)?s ==?P?S|什么?Q?S这些定义将命令(A,B,C)作为state→结果集类型的函数,将条件(P,Q)作为state→bool类型的函数。 我们注意到,一个命令(作为一个函数)是由它的wlp和终止条件唯一确定的。这在伊莎贝尔身上被证明是独一无二的。后来J.E. Dawson / Electronic Notes in Theoretical Computer Science 91(2004)21-27我们将介绍相应的(不同命名的)函数,其将语法树作为参数。在[1,§5]中,Dunne讨论了精化的几个概念,包括一般正确性精化、完全正确性精化和部分正确性精化。gencref的第二个等价定义来自Dunne的( Gcref 2 ) ( [ 2 , §2.1] ) 。 同 样 , ( A , B , C ) 是 命 令 , 类 型 为state→outcome set。totcref?一个?B ==所有Q。wpm?一个Q-> wpm?B Qpartcref?一个?B ==所有Q。wlpm?一个Q-> wlpm?BQ gencref?一个?B == partcref?一个?B&totcref?一个?Bgencref?一个?B == partcref?一个?B(trmm?A-> trmm?B)、从这些定义出发,我们证明了这三个精化概念的以下更直接的特征。值得注意的是,一般正确性的特征化比其他两个简单,尽管它是根据它们两者来定义的;这无疑解释了一般正确性语义如何经常看起来比部分或完全正确性语义更简单此外,一般的正确性关系是反对称的,不像完全或部分正确性。“托特克里夫?一个?B =(所有圣?B st =?A St|非术语:?Ast)”“partcref?一个?B =(所有圣?B st =插入NonTerm(?Ast))”“gencref?一个?B =(所有状态。?B状态=?Astate)”gencref_antisym =“[|gencref?一个?B; gencref?B?一|]==>?A =?B”3.3最强后置条件一些作者讨论了最强后置条件,在[6]中引用在[6]中,Lermer,Fidge Hayes给出了他们定义的命令的最强后置条件语义,以及最弱的自由前置条件语义,我们将在后面提到其中的一些同时,我们在《伊莎贝尔》中给出了它的定义,以及他们所谓的“slpm?C?P?说某人的坏话?P sb& Term?州:?你好吗?一个?B ==所有Q。slpm?BQ-> slpm?阿Q”也就是说,假设前提B被满足,slpmC(仅)对C的可能(终止)结果的那些状态成立。这显然类似于一个最弱的自由前提(因此我们称之为slpm),因为如果一个命令被改变以允许(或不允许)额外的非终止可能性事实上,证明(如wlp_slp_ref)最强后置条件加细等价于部分正确性加细( [6,Thm 6.1(vii)])是微不足道的。这很容易用最弱的自由主义前提和最弱的自由主义前提之间的伽罗瓦联系来解释。28J.E. Dawson / Electronic Notes in Theoretical Computer Science 91(2004)21-最强后置条件函数(wlp_slp_gal),其中定理6.1(v)和(vi)[6]是一个简单的推论。wlp_slp_ref =“partcref = slp”wlp_slp_gal =“(?Q-> wlpm?C?R)=(slpm?C?Q--->?R)”我们很可能会问,最弱的前提函数wp是否具有伽罗瓦对偶sp,但答案是否定的。 因为这需要sp C Q−→true(它总是成立)等价于Q−→wp Ctrue(它在满足Q但C不能终止的状态下不成立)。然而,我们可以定义函数spom和wpom(基于结果的最强后条件和最弱前条件),它们是伽罗瓦图,并且与一般正确性精化有很好的关系。注意,R是结果的谓词,Q是状态的谓词。spom:(state→outcome set)→(state→bool)→outcome→boolwpom:(state→outcome set)→(outcome→bool)→state→boolspomC Q c = 1000 Q s∈C swpomC R s =<$c∈C s. R cwpo_spo_gal =“(?Q -> wpom?C?R)=(spam?C?Q --->?R)”gencref_wpo =“gencref?一个?B =(所有Q. wpom?一个Q--->wpom?B Q)”gencref_spo =“gencref?一个?B =(所有Q. spom?BQ->spom?阿Q)”3.4命令的含义:skip,perhaps,magic,abort[1,§7]skip是一个可行的命令,它会终止,对状态不做任何事情。这正是unitos函数。从(左单位)和(右单位)单子定律可以直接得出,skip是二元函数 seq 的 恒 等 式 ( 左 和 右 ) 。 这 些 在 Isabelle 中 被 证 明 为 seq_unitL 和seq_unitR。我们也定义也许吧St=={Term什么?st,NonTerm}魔法?St=={}中止?St=={NonTerm}预处理命令[1,§7]命令P|A与A相同,只是如果P不成立,则P|A可能无法终止。预处理P?C?state ==如果?P?国,然后?C?stateelse insert NonTerm(?C?国家)J.E. Dawson / Electronic Notes in Theoretical Computer Science 91(2004)21-29保护命令[1,§7]如果P成立,则命令P−→A与A相同,但不可行(the结果集为空),如果P不成立。警卫?P?C?状态==如果?P?国,然后?C?状态else{}一个命令有一个这里fisA表示A是可行的,也就是说,它的结果集是非空的。 我们已经证明fis_guard =“guard(fis?A)?A =?一个”pc_trm =“预处理器(trmm?A)?A =?A”选择在[1,§7]中,Dunne定义了一个二元运算符AQB,用于有界选择:AQB是一个可以在两个命令A和B之间选择的命令。这是在任意一组命令中选择的特殊情况,定义如下:选择C s=c∈Ccs选择?C?state == UN C:?CS. C?状态由此,我们证明了Dunne [2,§ 5,6]的定义和其他结果。perhaps_alt =“perhaps = precon(%st. False)unitos”magic_alt =“magic = guard(%st. False)?A”abort_alt =“abort = precon(%st. False)(guard(%st. False)?A)”pma =“seq perhaps magic = abort”asp =“choice {abort,unitos} = perhaps”音乐会[1,§12]命令A#B表示A和B在状态的不同副本上独立执行:A或B中最先终止的一个给出A#B的结果。因此,A#B的可能结果是:• 项s,如果它是A的结果,• 项s,如果它是B的结果,• NonTerm,如果它是A和B的结果。conc?一个?B?state == concrs(?一个?state)(?B?州)concrs?cr1?cr2 ==?cr1 Un?cr2- {NonTerm} Un {NonTerm}Int?cr1Int?CR2有趣的是,这意味着如果B是魔术(处处不可行),那么A#B只是A,没有任何不终止的可能性(尽管从上面的第一句话就可以看出这很难这在Isabelle中被证明为conc_magic。30J.E. Dawson / Electronic Notes in Theoretical Computer Science 91(2004)21-Dunne用来定义这些命令的wlp和终止条件在Isabelle中根据我们的定义证明 为 precon_trm , precon_wlp , guard_trm , guard_wlp , seq_trm ,seq_wlp,choice_trm,choice_wlp,conc_trm和conc_wlp。DunneXpre =“seq(precon?P?A)?B =预处理?P(seq?一个?B)”Xguard =“seq(guard?P?A)?B =守卫?P(seq?一个?B)”Xcup =“guard?P?A = seq(guard?P unitos)?一个”Xassert =“precon?P(警卫?P?A)=seq(precon?P(警卫?P unitos))?A”3.5重复和迭代有限重复[1,§7] Dunne定义了A0=skip和An+1=A;An。我们证明的一个非常方便的结果,称为rep_Suc重复闭合[12]我们还定义了repallc s=n代表n c s,即,repall?C?联合国国家代表?C?状态也就是说,repallA是任何重复次数的(无界)选择,A. repallA的终止条件是对于每个n,An终止(证明为repall_term)。A的重复闭包是A,其中A的结果是repall的结果,在可以无限次顺序执行A的情况下,增加NonTerm得多在操作上比在wlp和trm方面更容易定义这一概念。无限链的定义断言了一个无限状态序列,其中每个状态都可以从前一个状态到达。我们忽略了伊莎贝尔的定义。infchA ssamplef. f 0 = s(n. 项(f(n+ 1))∈A(f n))因此,我们有定义,repstar?C?state == repall?C?国家联合国(if infch?C?state then {NonTerm} else{})可以注意到,在[1,§10]中,Dunne定义了谓词cic(“循环和无限链”),其意图是如果A的永久重复是可行的,则cic A为真(即,A的无限执行链是可能的然而,这个定义使得cicAs在A可能是J.E. Dawson / Electronic Notes in Theoretical Computer Science 91(2004)21-31顺序地执行任何给定的n次,这不足以确保执行的无限链。(It在有界不确定性的假设下是足够的,见[4,§3])。作为一个常见的经验,我们没有发现这种差异,直到试图执行伊莎贝尔证明的基础上的定义问题。我们已经证明了一些有用的结果,如wlpca:wlp(A_i)=wlp(repallA_i)(因为它们的不同之处仅在于A_i具有非终止的附加可能性)seq repstar:A;A=A;A在[1,§12]中,Dunne提到重复闭合可以定义为:Egli-Milner近似[1,§6].A≤emAJ <$A±totAJ <$AJ±parA其中±tot和±par分别表示总体和部分正确性修正。故A是在≤em序下的最小定点:一个X. (A;X)Q跳跃我们在《伊莎贝尔》中表明,我们对A的定义隐含了这个结果。这里fprep_alt2是我们对fprep(fprepA)定义的一种解释X表示X =(A; X)Q skip),repstar_isfp表示A是定点,repstar_is_lfp表示A在Egli-Milner排序中小于或等于任何给定定点Y。我们还知道Egli-Milner排序是反对称,所以最小定点是唯一的。fprep_alt2 =“fprep?一个?X =(?X =选择{seq?一个?X,unitos})”repstar_isfp =“fprep?A(repstar?A)”repstar_is_lfp =“fprep?一个?Y ==> egMil(repstar?A)?Y”egMil_antisym=“[|egMil?一个?B; egMil?B?一|]==>?A =?B”Dunne(pers. comm.) 也将trm(A)和wlp(A,Q)定义为固定点:trm(A)= νY。wp(A,Y)wlp(A,Q)= µY。wlp(A,Y)其中,最小和最我们也证明了这些结果在伊莎贝尔,基于我们对A的定义。trfp和wrfp说trm(A)和wlp(A,Q)是各自函数的定点。trsfp说trm(A)等于或弱于任何给定的定点Y,对于wrwfp也是如此。trfp =“trmm(repstar?A)= wpm?A(trmm(repstar?A))”trsfp =“?Y= wpm?一个?Y==> trmm(repstar?A)->?Y”32J.E. Dawson / Electronic Notes in Theoretical Computer Science 91(2004)21-wrfp =“let wlpstar = wlpm(repstar?A)?Q在wlpstar =(wlpm?一个wlpstar?&&Q)”wrwfp =“?Y =(wlpm?一个?是&&吗 ?Q)==>?Y -> wlpm(repstar?A)?Q”对于repall,我们可以得到一组类似的结果。首先,repallA是一般正确性修正序±gen下的最大定点,其次,repallA的终止条件是最小(最弱)定点。回想一下wlp(repallA,Q)=wlp(Arepall,Q)。repallA = vgenX。(A; X)Q skip trm(A)= µY。wp(A,Y)repall_isfp =“fprep?A(repall?A)”repall_is_gfp =“fprep?一个?X ==> gencref ?X(repall?A)”trallfp =“trmm(repall?A)=wpm?A(trmm(repall?A ) ) ”trallwfp =“ ? Y =wpm ? 一 个 ? Y ==> ? Y-> trmm(repall?A)”因此,repallA和A都是λX的± par下的最大定点。 (A; X)Q跳过,表示这样的定点不需要是唯一的,因为±par不是反对称的。3.6单调性为了开发一个程序,从一个抽象表达式(需求)开始,并逐步将其细化为一个具体的程序,重要的是抽象命令构造函数对于一般正确性细化(±gen)是单调的。给定我们对A±genB的描述为(A状态.B状态<$A状态),以及我们根据结果集对命令的操作定义,很容易看出所有提到的构造函数都是单调的。在任何情况下,它们在Isabelle中被证明为(例如)seq_ref_mono,repstar_ref_mono等。3.7while循环在[1,§7,§12] Dunne定义中,如果G然后A结束<$(G→A)Q(<$G→skip),而G做A结束<$(G→A)<$;<$G→skipwhile的定义对程序员来说很直观,当G做A结束时 ≡ 如果G那么A;而G做A结束结束我们不能在Isabelle中使用它作为定义,因为它是递归的,它是非终止的,当应用于特定状态时,可以J.E. Dawson / Electronic Notes in Theoretical Computer Science 91(2004)21-33而不是终止。因此,在《伊莎贝尔》中,我们和邓恩一样定义了whilewhile_prog =“while?G?A =如果?G(seq?A(while?G?(A))”4框架和变量名在第3节中,我们把命令看作是从状态到结果集合的函数,把条件看作是状态的谓词。在这种处理中,国家的观点是抽象的。正如第2节所讨论的,有各种方式需要更具体地进行全面处理,即• 引用程序变量• 具有允许替换程序变量• 为命令在本节中,我们将讨论那些需要我们解决这些问题的抽象命令构造函数在我们的Isabelle模型中,程序变量名是'n类型由于状态是变量到值的赋值,我们有类型定义state=name→value,或者,在Isabelle中,state =不定赋值[1,§12]其中x是变量(列表),P是谓词,命令x:P以任何方式为x中的变量赋值,使得变化 国家满意度P。更准确地说,如果α是(The论文[1]说α<$α0带下标的变量名表示这些变量在执行命令之前的值我们将这样的P建模为状态关系,因此我们将此命令定义为“indetass?vars?P?state ==术语'((?我的名字?vars)状态})”CHST在哪里?vars是指状态对的集合,这些状态对只在变量上不同。vars,f' X表示集合X在函数f下的像,r "X表示X在关系r下的“像”,即,{y|(x,y)∈r,对于x∈ X}.虽然Dunne没有给出不确定赋值的wlp,但Ler- mer,FidgeHayes [6](他们对Dunne的x:P使用符号x:[P]34J.E. Dawson / Electronic Notes in Theoretical Computer Science 91(2004)21-其中xJ是指执行命令后变量xwlp(x:Q,R)=<$xJ.Q→R[x:=xJ]sp(x:Q,R)=(<$x.R<$Q)[xJ:=x]这些在伊莎贝尔身上很难表达。这是因为……意思是“.在某种意义上,这是符号x的重载,这使形式化复杂化。然而,我们得到了以下结果的wlp和sp的不确定分配,这是在一个相当接近的形式上的表达式。我们使用一个函数setvars,类型为set→state→state→state,它重置给定集合中变量的值,我们引用第二个状态,来表示xJ中的值。setvars?vars?准备好了吗州?字符串==如果?str:?那么,vars?准备好了吗还有别的吗?州?string indetass_wlp' =“wlpm(indetass?x?Q)?R?state =(ALL准备好了 (?国家,setvars?x准备好了吗state):?Q -->?R(setvars?x准备好了吗国家))”indetass_slp' =“slpm(indetass?x?Q)?R?启动=(EX状态(setvars?x州?准备好了吗?primed):?Q&?R(setvars?x州?primed))”PRD[1,§10]邓恩将其定义为prd(A)wlp(A,xi=xJ)其中XJ是对应于程序变量X的新(逻辑)变量。我们将prds和prdm定义为prds?vars?准备好了吗A ==不是吗?A(% st. EX str:?瓦尔斯st str ~=?primedstr)prdm?准备好了吗A == Not o wlpm?A(% st. st ~=?(primed)在哪儿?state类型的primed表示值xJ,prdm是prds的一个更简单的版本,用于当x可以被认为是所有变量名时使用。Dunne还给出了wlp在prd方面的wlp(A,Q)=xJ。prd(A)<$Q[x:=xJ],我们证明为wlp_prd =“wlpm?一个?Q?state =(ALL准备好了prdm准备好了吗?一个?状态-->?Q启动)”J.E. Dawson / Electronic Notes in Theoretical Computer Science 91(2004)21-35在[2,§9]中,Dunne指出结果prd(x:P)=P[x0,x:=x,xJ]。对于x表示所有变量名的特殊情况,我们证明了一个相应的结果indetass_prd =“prdm?启动(indetass UNIV?P)?state =((?国家,?primed):?P)”但发现我们不能普遍地证明所述结果。结果证明Dunne这是另一个常见情况的例子,即试图正式证明这样的结果会发现这样的点,这些点在非正式的处理中很容易被忽视。无限选择[1,§7]命令(@z. A)意味着变量z被设置为任意值,然后A被执行。但是z是A中的一个换句话说,这个符号正确地反映了z对于一个绑定变量的行为是正常的(它可以被α转换而意义没有改变)。所以我们对这个命令建模如下:• 使用setvars将变量z• 执行• 使用revert将变量z回复?vars?一个?初始化==mapos(setvars?vars?initst)(?一个?initst)在?vars?一个?初始化==设initptf= %primed。setvars?准备好了吗initst; initptc= %x. UNION UNIV(?A oinitptf)反过来呢?vars initptc?初始化这里,UNION UNIVF=xF x,mapos是一元maposf ocset ={mapo f s |s ∈ ocset}映射f(Term s)= Term(f s)mapofNonTerm=NonTerm然后我们证明了at_trm =“trmm(at?vars?A)=所有变量?vars(trmm?A)”其中,allvarsvarsB s意味着对于通过取s并将变量vars设置为任何值而获得的任何其他状态sJ,B sJ成立。 由于Dunne给出wlp(@ z. A,Q)=zz.wlp(A,Q),我们试图证明wlpm(at?vars?A)?Q =所有变量?vars(wlpm?一个?Q)36J.E. Dawson / Electronic Notes in Theoretical Computer Science 91(2004)21-但是不能。这反映了Dunne给出的wlp(@z. A,Q)的公式假定Q不涉及z。(As如上所述,z在@z. A中的α-可转换性意味着我们可以合理地假设这一点)。事实上我们证明了更复杂的结果at_wlp =“wlpm(at?vars?A)?Q?st =(所有st.wlpm?A(?Q o setvars?vars?st)(setvars?什么事?st))”at_slp =“slpm(at?vars?A)?Q?st=(EX nst.slpm?A(?Qo setvars?vars?st)(setvars?什么事?st))”Lermer,Fidge Hayes [6]给出了一个类似的命令(使用它们的框架涉及类型化变量和在“上下文”中执行命令,但是如果去掉这些方面,它们的表达式就wlp(@ z. A,Q)=(λz. wlp(A,Q[z:=y]))[y:=z]sp(@ z. A,Q)=(λz. sp(A,Q[z:=y]))[y:=z]其中y表示在A或Q中不出现(自由)的新变量。现在我们将这些结果与我们的结果进行比较。(i) 首先,虽然Q[z:=y]指的是变量y对变量z的文本替换,但我们可以这样解释:Q[z:=y]s表示取状态s,将值y(即,将y视为逻辑变量)赋给程序变量z,然后将谓词Q应用于结果状态。因此,我们可以说Q[z:=y]=Qsetvarsz y,注意右边的y是对所有变量的赋值-(ii) 接下来,我们解释(z.P)s,其中P是关于状态的谓词。这意味着P sJ对于通过将程序变量z设置为其他值x而从s获得的每个状态s j都成立。也就是说,(z.P)s=x。(Psetvarsz x)s.(iii) 最后,我们需要解释R[y:=z]s,因为R是一个包含逻辑变量y的谓词。这需要用程序变量z在状态s中的值替换R中出现的y。幸运的是,我们发现y只出现在子表达式setvarsz y(在一个状态下将z重置为y的函数)中;在这个特定的表达式中,用s中z的值替换y只会得到setvarsz s。我们也可以 说 我 们 得 到 setvarsz ( setvarsz s y ) , 我 们 已 经 证 明 ( 作 为setvars_set)等于setvarsz s。J.E. Dawson / Electronic Notes in Theoretical Computer Science 91(2004)21-37因此,下面的结果证明了我们的结果与[6]中的结果是等价的.(z. wlp(A,Q[z:=y]))[y:=z]s=(z. wlp(A,Q)[y:=z]s(by(i))=10x。(wlp(A,Qsetvarsz y)setvarsz x)[y:=z]s(by(ii))=10x。wlp(A,Q=setvarsz s)(setvarsz x s)(by(iii))4.1语法观(Syntagical View)如§2所述,wlp(x:=E,Q)=Q[x:=E],这仅在以下情况下有意义: Q是某种结构,我们可以在其中定义替换(尽管我们已经用QsJ模仿了Q[x:=E]s,其中sJ是与s相同的状态,除了变量s被赋予E的值)。因此,我们定义了表达式(exp)和布尔表达式(bexp)的抽象语法树版本的类型,因此:datatype| Op“ 'v l i s t = > 'v ” “ ( 'n , 'v ) e x p l i s t ”| 瓦尔恩datatype| Brel“bool list => bool”“('n,'v)bexp list”因此,表达式是一个简单的值,或者是一个对值的操作和一个参
下载后可阅读完整内容,剩余1页未读,立即下载
cpongm
- 粉丝: 5
- 资源: 2万+
上传资源 快速赚钱
- 我的内容管理 展开
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
最新资源
- WebLogic集群配置与管理实战指南
- AIX5.3上安装Weblogic 9.2详细步骤
- 面向对象编程模拟试题详解与解析
- Flex+FMS2.0中文教程:开发流媒体应用的实践指南
- PID调节深入解析:从入门到精通
- 数字水印技术:保护版权的新防线
- 8位数码管显示24小时制数字电子钟程序设计
- Mhdd免费版详细使用教程:硬盘检测与坏道屏蔽
- 操作系统期末复习指南:进程、线程与系统调用详解
- Cognos8性能优化指南:软件参数与报表设计调优
- Cognos8开发入门:从Transformer到ReportStudio
- Cisco 6509交换机配置全面指南
- C#入门:XML基础教程与实例解析
- Matlab振动分析详解:从单自由度到6自由度模型
- Eclipse JDT中的ASTParser详解与核心类介绍
- Java程序员必备资源网站大全
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功