公理语义 一个语言的每个语法成分的含义定义为公理和演绎规则, 用于推导出该成分执行的效果 公理语义概念是随着程序正确性的证明而发展的。当正 确性证眀能构造时表明程序执行它的规格说明所描述 的计算。在一个证明中,每一个语句之前之后都有 个逻辑表达式对程序的变量进行约束,以此说明这个语 句的含义 般的记号{P}SQ} 如果在语句S执行前P为真,则在语句S执行并终止后Q为 真
公理语义 一个语言的每个语法成分的含义定义为公理和演绎规则， 用于推导出该成分执行的效果。 公理语义概念是随着程序正确性的证明而发展的。当正 确性证明能构造时表明程序执行它的规格说明所描述 的计算。在一个证明中，每一个语句之前之后都有一 个逻辑表达式对程序的变量进行约束,以此说明这个语 句的含义。 一般的记号 {P} S {Q} 如果在语句S执行前P为真，则在语句S执行并终止后Q为 真
演绎规则的例子 规则前驱 后继 赋值:x=expr ( P(expr)x: expr(P(x) While:{P∧B}S{P} iPi while b do s end P A(not B) if--then--else B∧P}Sn{Q},{(notB)∧P}S2{Q} (P if b then Si else $ Q)
演绎规则的例子 规则 前驱 后继 赋值：x:=expr {P(expr)}x:=expr{P(x)} While: {P ∧ B} S {P} {P} while B do S end {P ∧ (not B)} if--then--else {B ∧ P} S1 {Q}, {(not B) ∧ P} S2 {Q} {P} if B then S1 else S2{Q}
指称语义 指称语义的基本概念是给每一段程序实体定义一个数 学意义上的对象,和一个从实体实例向数学意义对象 的映射的函数 特点:不但对全部程序赋予全文而且对程序设计语法 每一个语法成分短语(表达式,命令,声明..) 都给予含义。 每一个语法成分(短语)的含义是以它的自 成分的含义的术语来定义的。 即语义结构平行于语法结构 语义函数:程序设计语言的语义利用映射函数来证 明 语义函数将短语映射到它的指称
指称语义 • 指称语义的基本概念是给每一段程序实体定义一个数 学意义上的对象，和一个从实体实例向数学意义对象 的映射的函数 • 特点： 不但对全部程序赋予全文而且对程序设计语法 每一个语法成分短语（表达式，命令，声明…） 都给予含义。 每一个语法成分（短语）的含义是以它的自 成分的含义的术语来定义的。 即 语义结构 平行于语法结构。 • 语义函数： 程序设计语言的语义利用映射函数来证 明。 语义函数将短语映射到它的指称
例 二进制数语言110或10101语法实体 指称(自然数)6或21语义实体 二进制数文法 Numeral:=0 :=1 NM umbral O umbral 1 自然数 Natrual={0,1,2,3,} 语义函数 Valuation: Numeral->Natural
• 例： 二进制数语言 110或10101 语法实体 指称（自然数） 6 或 21 语义实体 二进制数文法 Numeral::=0 ::=1 ::= Numeral 0 ::=Numeral 1 自然数 Natrual={0,1,2,3,…} 语义函数 Valuation:Numeral→Natural
Valuation[101]表示把 Valuation施用于101 Valuation NI 把它施用于N 定义: Valuation(用四个方程为有四个形式 numeral Valuation[o]=0 Valuation[l] Valuation[N0]≡2× Valuation[N] Valuation]≡2× Valuation[N]+1 所以: Valuation[ 110]=2 X Valuation[ 11] 2×(2× Valuation[1]+1) 2×(2×1+1)
• Valuation[101] 表示把Valuation施用于101 Valuation[N] ------ 把它施用于N 定义: Valuation（用四个方程)因为有四个形式numeral Valuation[0] 0 Valuation[1] 1 Valuation[N0] 2Valuation [N] Valuation[N1] 2Valuation [N]+1 所以： Valuation[110]=2 Valuation[11] = 2 (2 Valuation[1]+1) =2 (2 1+1) =6