我正在阅读一篇非常愚蠢的论文,并继续谈论乔托如何定义"形式语义".
Giotto具有正式的语义,指定模式切换,任务间通信以及与程序环境通信的含义.
我处于边缘,但却无法完全理解"形式语义"的含义.
Mic*_*son 12
为了扩展Michael Madsen的答案,一个例子可能是++运算符的行为.非正式地,我们使用普通英语描述运算符.例如:
如果
x是类型的变量int,则++x使x增加1.
(我假设没有整数溢出,并且++x不会返回任何内容)
在一个正式的语义中(我将使用操作语义),我们还有一些工作要做.首先,我们需要定义类型的概念.在这种情况下,我将假设所有变量都是类型int.在这种简单的语言中,程序的当前状态可以由存储来描述,存储是从变量到值的映射.例如,在程序中的某个点,x可能等于42,而y等于-5351.商店可以用作函数 - 例如,如果商店s的变量x值为42,那么s(x) = 42.
程序的当前状态还包括我们必须执行的程序的其余语句.我们可以将其捆绑为<C, s>,C剩下的程序在哪里,并且s是商店.
因此,如果我们有状态<++x, {x -> 42, y -> -5351}>,这是一个非正式的状态,其中唯一剩下的执行命令是++x,变量x具有值42,并且变量y具有值-5351.
然后我们可以定义从程序的一个状态到另一个状态的转换 - 我们描述当我们在程序中执行下一步时会发生什么.因此,++我们可以定义以下语义:
<++x, s> --> <skip, s{x -> (s(x) + 1)>
有点非正式地,通过执行++x,下一个命令是skip没有效果的,并且商店中的变量没有变化,除了x,它现在具有它最初具有的值加1.还有一些工作要做,例如定义我用来更新商店的符号(我没有这样做以阻止这个答案变得更长!).因此,一般规则的具体实例可能是:
<++x, {x -> 42, y -> -5351}> --> <skip, {x -> 43, y -> -5351}>
希望这会给你一个想法.请注意,这只是形式语义的一个例子 - 除了操作语义,还有公理语义(通常使用Hoare逻辑)和指称语义,还有更多我不熟悉的东西.
正如我在对另一个答案的评论中提到的,形式语义的一个优点是你可以使用它们来证明程序的某些属性,例如它终止.除了显示您的程序没有表现出不良行为(例如非终止)之外,您还可以通过证明您的程序与给定规范匹配来证明您的程序的行为符合要求.话虽如此,我从未发现指定和验证程序的想法都令人信服,因为我发现规范通常只是在逻辑中重写的程序,因此规范也很可能是错误的.
形式语义描述语义 - 以及正式方式 - 使用以明确方式表达事物含义的符号.
它与非正式语义相反,它基本上只用简单的英语描述一切.这可能更容易阅读和理解,但它会产生误解的可能性,这可能导致错误,因为有人没有按照您打算阅读它的方式阅读段落.
编程语言可以同时具有正式和非正式语义 - 非正式语义可以作为形式语义的"纯文本"解释,如果你不确定什么是非正式的解释,那么正式的语义就是你要看的地方.真正意思.