tailieunhanh - Concepts, Techniques, and Models of Computer Programming - Chapter 13

Language Semantics Đối với tất cả các mô hình tính toán của các chương trước, chúng tôi đã đưa ra một ngữ nghĩa chính thức về của một máy trừu tượng đơn giản. Đối với mô hình khai báo, điều này máy tính trừu tượng bao gồm hai phần chính: một cửa hàng duy nhất phân công và ngăn xếp một ngữ nghĩa. Đồng thời, chúng tôi mở rộng các máy tính để có các ngăn xếp nhiều ngữ nghĩa. Để thực hiện lười biếng, chúng tôi đã thêm một cửa hàng kích hoạt. Đối với nhà nước rõ ràng,. | Part IV Semantics Copyright @ 2001-3 by P. Van Roy and S. Haridi. All rights reserved. Chapter 13 Language Semantics This is the secret meaning of the runes I hid here magic-runes undisturbed by evil witchcraft. In misery shall he die by means of magic art who destroys this monument. - Runic inscription Bjorketorp Stone For all the computation models of the previous chapters we gave a formal semantics in terms of a simple abstract machine. For the declarative model this abstract machine contains two main parts a single-assignment store and a semantic stack. For concurrency we extended the machine to have multiple semantic stacks. For lazy execution we added a trigger store. For explicit state we added a mutable store. For read-only views we added a read-only store. This chapter brings all these pieces together. It defines an operational semantics for all the computation models of the previous We use a different formalism than the abstract machine of the previous chapters. The formalism of this chapter is more compact and easier to reason with than the abstract machine definitions. It has three principal changes with respect to the abstract machine of Chapter 2 It uses a concise notation based on reduction rules. The reduction rules follow the abstract syntax . there are one or more rules for each syntactic construct. This approach is called Structural Operational Semantics or SOS for short. It was pioneered by Gordon Plotkin 208 . It uses substitutions instead of environments. We saw that statements in order to be reducible must define bindings for their free identifiers. In the abstract machine these bindings are given by the environment in the semantic statement. In this chapter the free identifiers are directly substituted by references into the store. We have the invariant that in a reducible statement all free identifiers have been replaced by store references. 1This chapter was co-authored with Raphael Collet. Copyright 2001-3 by P. Van Roy and