The focus of these lecture notes is on abstract models and basic ideas and results that relate to the operational semantics of programming languages largely conceived. The approach is to start with an abstract description of the computation steps of programs and then to build on top semantic equivalences, specification languages, and static analyses. While other approaches to the semantics of programming languages are possible, it appears that the operational one is particularly effective in that it requires a moderate level of mathematical sophistication and scales reasonably well to a large variety of programming features. In practice, operational semantics is a suitable framework to build portable language implementations and to specify and test program properties. It is also used routinely to tackle more ambitious tasks such as proving the correctness of a compiler or a static analyzer.
翻译:本讲义重点探讨与广泛构想的编程语言操作语义相关的抽象模型、基本思想及核心结果。该方法从程序的抽象计算步骤描述出发,在此基础上构建语义等价关系、规约语言与静态分析。尽管编程语言语义学存在其他研究路径,但操作语义方法因其所需的数学复杂度适中,且能良好适配各类编程特性而显得尤为有效。实践中,操作语义学是构建可移植语言实现、规约与验证程序属性的适宜框架,亦常规应用于编译器正确性证明、静态分析器验证等更复杂的任务。