稳健规范仍然是它的编译器吗？

Question

我目前正在阅读一些有关智能合同验证的文献。我读过的一篇论文是交互式定理证明器的虚机器定义，Hirai (pirapira)写的。在关于稳固性的考虑(第2.1节)中，他说：

Solidity有一个reach语法，但没有规范。Solidity的唯一定义是Solidity编译器实现。

我想知道这是否仍然是这样，或者在此期间发生了一些变化。

我看到kframework团队已经开始定义K框架下的固体语义了

Answer 1

每一次更新都会改变稳健性的语义，唯一的规范定义是编译器本身。注意，编译器的预期行为和实际行为是有区别的，这有时会导致编译器错误。那么，更准确的说法是，稳健语义的(非正式)定义在文档中。