AnyMath 文档

Promela语法

下面仅描述用于生成模型的Promela语言的基本构造。 AnyMath 或有用的分析生成的代码。 Promela*语法，用于并行程序的规范，在 *AnyMath 这里没有涉及，也很少考虑。

一般（词汇）信息: Promela中的标识符满足正则表达式 [a-zA-Z_][a-zA-Z_0-9]; *因为 旋转 可用的C语言预处理器用作预处理器，支持ISO C99标准的多行和单行（未记录功能）注释。

Promela语言中源文件的结构

Promela语言的程序文本可以由三个主要部分组成:

*定义自定义数据类型和全局变量; *过程定义; *运营商 零担.

用户定义的数据类型和全局变量的定义

在Promela中，用户定义的数据类型和全局变量的定义可以穿插，但必须放在文件的开头-在进程和运算符的定义之前。 零担.

自定义数据类型

Promela代码生成器在 AnyMath 仅使用一个Promela构造，用于定义自定义数据类型 — 打字,打字，用于定义数据结构的类型。

语法 打字,打字，由 AnyMath :

"typedef" name "{" declaration_list "}" ";"

哪里 姓名 -不是的标识符 关键词Promela和语法 声明_列表 它有表格:

declaration_list ::= declaration ";" { declaration ";" }

declaration ::= type_name variable_name [ "[" array_size "]" ]

type_name ::= "bool" | "byte" | "short" | "int"

variable_name ::= name

array_size ::= constant_expression

常量表达式 -具有整数值的常量表达式。

例如，结构类型声明 S，其中包括: *32位字段 我32 有符号整数类型; *16位字段 我16 有符号整数类型; *8位字段 u8 无符号整数类型; *1位字段 b 无符号整数（逻辑）类型; *阵列 a 的10个逻辑类型元素。

可谓

typedef S {
    int i32;
    short i16;
    byte u8;
    bool b;
    bool a[10];
};

随着语法的更详细的描述 打字,打字 可于 项目页Promela/纺.

全局变量

Promela中定义全局变量的语法如下所示:

global_variable_declaration ::=
    type_name variable_name [ "=" initializer_scalar ] ";"
|   type_name variable_name [ "[" array_size "]" ] [ "=" initializer_list ] ";"

initializer_scalar ::= constant_expression

initializer_list ::= "{" constant_expression [ "," constant_expression ]* "}"

语法 类型名称, 可变名称, array_size 和 常量表达式 如上所述。

可以定义标量变量、一维数组和变量结构。

例如，下面的代码定义了一个变量-一个由5个类型元素组成的数组 字节，用单位初始化:

byte x[5] = {1, 1, 1, 1, 1};

如果标量变量未显式初始化，则 旋转 将其初始值设置为零，如果它是数组或结构，则用零填充其元素。

定义流程

用Promela语言生成模型时 AnyMath 定义单一类型的流程: fsm （来自"有限状态机"）。

active proctype fsm() { ... }

这意味着过程 fsm 它将在模式中的单个实例中运行 模拟。 如果使用模式 验证，然后是过程的描述 fsm，与LTL规范一起，转换为自动机，将由生成的验证器进行分析。

过程描述的主体由一系列运算符组成，例如局部变量的定义、赋值运算符和程序流控制运算符。

在Promela中，运算符在语义上分为阻塞和非阻塞，但在Promela中，它们是由生成器生成的模型。 AnyMath ，只使用非阻塞运算符。

局部变量的定义

定义Promela局部变量的语法与 语法全局变量的定义。

无论局部变量定义运算符放置在何处：在过程主体的开始处或在第一次使用之前，执行变量定义，就好像它位于过程主体的开始处一样。

这意味着您不能定义多个具有相同名称的局部变量。 例如:

{ int a; }
{ int a; }

在这种情况下，在声明变量的上下文中执行局部变量的初始化。 即示例中的代码:

int a = 1;
{
    a = 2;
    int b = a + 1;
}

语义上等同于代码:

int a = 1;
int b;
a = 2;
b = a + 1;

不是代码:

int a = 1;
int b = a + 1;
a = 2;

赋值运算符

在赋值运算符的左侧，可以使用标量变量、数组元素或结构的名称。

右侧是包含变量名，逻辑或整数常量的算术或逻辑表达式。

还支持增量运算符（++）和递减（--).

逻辑表达式

生成Promela模型时 AnyMath 可以使用逻辑连接词:

*否认 — !; *连词（逻辑和） — &&; *析取（逻辑或） — ||.

此外，可以使用比较运算符。 ==, !=, <, ⇐, > 和 >=.

逻辑运算符的参数可以是整数或逻辑类型的表达式。

算术表达式

在Promela代码生成器 AnyMath 实现以下整数算术运算：一元 + 和 - 加减乘除模（%).

由于代码生成器使用Julia语言中的表达式作为源表达式，其中除法的结果是类型 浮子,浮子，并且除法运算符Promela中不支持浮点计算 / Promela模型代码生成器未实现。

执行流控制语句

Promela代码生成器可以使用三种类型的控制运算符语法：条件运算符 如果 和两个循环运算符 做 和 为.

条件运算符 如果

在Promela，运营商 如果 它是一种非确定性的 link:https://en.wikipedia.org/wiki/Guarded_Command_LanguageEdsger Dijkstra的[条件运算符]:

if_operator ::= "if" guarded_command_set "fi"

guarded_command_set ::= guarded_command { guarded_command }

guarded_command ::= guard "->" guarded_list

guard ::= boolean_expression | "else"

guarded_list ::= statement ";" { statement ";" }

哪里 声明 --任何Promela操作员，以及 布尔值_表达式 — 逻辑表达。

Promela模型的代码生成器不使用非确定性运算符编程的功能 如果 因此，每个这样的运算符看起来像这样:

if
:: <условие> -> <действие>
:: else -> <альтернативное_действие>
fi

如果没有替代操作，则将其替换为空运算符。 跳过.

一个分支 其他 即使在没有替代动作的情况下也有必要，否则模型可能会被阻止。

例如，操作员

if
:: false -> ...
fi

相当于永恒的等待。

循环运算符 做

在Promela，运营商 做 它是另一个非确定性算子的变体。 — link:https://en.wikipedia.org/wiki/Guarded_Command_LanguageEdsger Dijkstra的[循环运算符]具有类似的语法:

do_operator ::= "do" guarded_command_set "od"

哪里 guarded_command_set 描述的 上。

Promela模型的代码生成器使用循环的确定性版本 做，其中可以有两个分支:

do
:: <условие> -> <действие>
:: else -> break;
od

它相当于一个循环 而:

while (<условие>) {
    <действие>;
}

或一个分支:

do
:: true -> <действие>
od

其对应于无限循环。

循环运算符 为

Promela代码生成器使用三种语法选项之一 为:

for_operator ::= "for" "(" variable_name ":" integer_expression ".." integer_expression ")" "{" statement_list "}"

statement_list::=语句";" { statement ";" }

哪里 可变名称 -本地或全局变量的名称，以及 集成表达式 -具有整数或布尔值类型的表达式。

例如，运算符的语义如下:

for (i : a .. b) {
    x = x + i;
}

以下是表达式 a 和 b 在循环之前计算一次，如果 a⇐b，一个变量 i 始终如一地接受来自 a 以前 b 包容性。

如果 a>b，则不执行循环。

无条件过渡运算符 后藤

Promela支持语法标签:

label_definition ::= label ":"

和无条件过渡算子:

goto_operator ::= "goto" label ";"

哪里 标签 --标签的名称，任何有效的标识符，除了 关键词。

一些标签名称具有特殊的含义 旋转：这些是带有前缀的标签 接受, 完和 进展。 Promela模型发生器在 AnyMath 不使用此类标签，建议避免不必要的标签。

不变量（断言）

除了LTL规范机制，Promela语言允许使用运算符进行验证 assert(<逻辑公式>) （有关详细信息，请参阅 断言）。

其语义类似于C/C++语言：如果运算符条件为false，则执行或验证失败。

操作员 断言 它很方便，因为它总是被检查，无论模式如何（模拟仿真 或 核实资料)和所选择的运算符 零担.

Promela关键词

不能用作标识符的保留字列表:

</*活动

*断言

*原子

*未签名

*布尔

*休息

*字节

*陈

*做

*d_step

*其他

*空

*已启用

*eval

*错误

*fi

*为

*已满

*后藤

*隐藏

*如果

*在

*init

*int

*莱恩

*mtype

*nempty

*永远不会

*nfull

*np_

*od

*的

*pc_value

*打印

*优先级

*proctype

*提供

*运行

*选择

*短

*展示

*跳过

*超时

*追踪

*真实

*typedef

*除非

*xr

*xs

*位

操作员组 零担

Promela中的源文本可能以由运算符组成的块结尾 零担.

运算符语法 零担:

ltl_operator ::= "ltl" name "{" ltl_formula "}"

哪里 姓名 -规格名称(LTL公式），以及 ltl_formula -一个人 LTL线性时间逻辑规范。

有关使用规范的更详细描述，请参阅章节 插入规格及 验证器的生成和启动。

有用的连结

  1. 正式核实 AnyMath

  2. Promela代在 AnyMath

  3. 自旋验证和规范模式

  4. 自旋中的线性时间逻辑(LTL)

  5. 形式验证的基本例子 AnyMath

  6. 形式验证的扩展示例 AnyMath