Imperative 的语法限制

为了使 imperative style 语言能用于推理，其必须只包含外部观察角度的纯函数。这样做是为了确保表达式的语义在不同上下文中是一致的，满足等式逻辑推理的条件。

具体而言，有以下几点要求：

不允许指针和全局变量： 避免引入指向内存位置的指针以及可能在程序各处影响的全局变量。这有助于确保函数的输入输出关系是可预测和可推导的。
数据结构不可变：
1. 由于规范不会实际执行，数据结构可以没有具体的内存模型，这允许定义归纳数据结构以替代原生的 struct。不可变性确保了数据结构的状态在函数调用间不会改变，从而简化了推理的复杂性。
允许对局部变量重新赋值（re-label）： 尽管数据结构内部是不可变的，但局部变量的重新赋值可以模拟状态的变化，提供更灵活的规范表达。
不允许带有副作用的子表达式（如 arr[k++]）：
1. 这一点确保了在函数调用以外的表达式中，子表达式的计算不会引入不确定的副作用。
2. 是否可以适当放宽这一限制取决于具体的推理需求。在命令式函数的内部，可以容许一定子表达式的副作用，只要这些副作用可以分离到表达式外部，如作为单独的语句提到表达式之前或之后。

归纳数据结构的例子：

enum list {
    nil,
    cons { 
        nat head; 
        list tail;
    }
}

实现相同的语义的 C 程序：

struct list {
    enum { nil, cons } tag;
    int head;
    list* tail;
}

萱草的博客