Page 97 - 《软件学报》2025年第9期

4008 软件学报 2025 年第 36 卷第 9 期

var ::= id|id[ra]|id[ra 1 ][ra 2 ]|la.var| pt → var

pt ::= la|&|(τ)ra|ra 1 +ra 2 |ra 1 −ra 2 |ext g(ra 1 ,...,ra n )|ext h(ra 1 ,...,ra n ,RVal)

la ::= var|∗ pt

ra ::= c|la|&|(τ)ra|mop 1 ra|ra 1 mop 2 ra 2 |if (b) then ra 1 else ra 2 |⊝ra|ext g(ra 1 ,...,ra n )|ext h(ra 1 ,...,ra n ,RVal)

mop 1 ::= +|−| ∼

mop 2 ::= +|−|∗| |%| ≪ | ≫ |&|| | ∧

b ::= true|false|ra 1 mrop ra 2 |¬b|b 1 ∧b 2 |b 1 ∨b 2

mrop ::=< | > | <= | >= | = |! =
其中, var、 id 为变量, pt 为指针表达式, τ 为类型, (τ)为类型转化 la 为左值表达式, ra 为右值表达式 ⊝ra 表示前
,
一状态 ra 的值, mop 1 为一元操作符, mop 2 为二元操作符, b 为布尔表达式, mrop 为关系操作符, ext g(ra 1 ,...,ra n )
ext h(ra 1 ,...,ra n ,RVal) 均表示外部调用, g 表示外部函数, h 表示用户自定义函数.
与
下面介绍 MSVL 的基本语句:
(1) 区间长度语句: empty,skip,len(n);
(2) 区间框架语句: frame(x);
(3) 并行语句: p||q;
(4) 顺序语句: p;q;
(5) 非确定选择语句: p or q;
(6) 合取语句: p and q;
(7) 等待语句: await(b);
(8) 立即赋值语句: x ⇐ e;
(9) 下一状态赋值语句: x := e;
(10) Always 语句: alw(p);
(11) Next 语句: next p;
(12) 循环语句: while(b) p;
(13) 条件语句: if (b)then p else q;
(14) 投影语句: (p 1 ,..., p m ) prj q;
(15) 函数调用语句: fun(e 1 ,...,e n );
(16) 外部函数调用语句: ext fun(e 1 ,...,e n );
其中, x 为变量, e 为算数表达式, b 为布尔表达式, p 1 ,..., p m , p,q 为 MSVL 语句.
empty,skip,len(n) 分别声明了当前区间长度为 q 在当前状态下
区间长度语句 0, 1, n; 并行语句 p||q 表明 p 与
同时开始执行, 并有可能在不同时间结束; 非确定选择语句 p or q 表示在当前状态下可以执行 p 或 q 中的任意一个;
顺序语句 p;q 表示 p 与 q 按照顺序执行; 合取语句 p and q 表示 p 与 q 在当前状态下同时开始执行并同时结束; 等
await(b) 将会循环判断表达式 b 的真假, 直到 b x ⇐ e 与下一状态赋值语句
待语句 为真时结束循环; 立即赋值语句
p next p 表示在下一状态
x := e 分别表示在当前状态和下一状态对变量进行赋值; alw(p) 表示在所有状态下执行 ;
执行 ; , 不仅包含赋
p while(b) p if (b)then p else q 以及函数调用语句的用法与其他高级程序设计语言相同. MSVL
值语句、循环语句、条件判断语句等基本语句, 还加入了框架结构和投影结构, 为描述软硬件系统提供了更强的
表达能力, 区间框架语句 frame(x) 使得变量 x 的值能够在区间上自动遗传, 否则变量 x 仅在被赋值时的状态下有
q
确定的值, 在其他状态下变量值是不确定的; 投影语句 (p 1 ,..., p m ) prj q 使得 p 1 ,..., p m 与 能够并行执行, 且
p 1 ,..., p m 顺序执行, 而 q 在另一个状态区间上执行.

1.2 MSVL 操作语义
定义 MSVL 程序 P m 的格局为四元组 (P m ,σ i−1 , s i ,i), 其中区间 σ i−1 记录了 < s 0 ,..., s i−1 > 中所有状态的信息, s i