The objective of this course is to provide the basic techniques to study the semantics of programmes/models. This enables the students the ability to understand semantics specifications, and hence understand design principles of programing lanuages, and to develop semantics for new languages. Formal semantics is the basis for any logical reasoning. The fundamental question to answer is how to justfiy formally based on the semantics whether a program/model satisfies certain property or two programs/models are equivalent or not.
This course describes and compares various semantic models. In particular, it covers 1) operational semantics which describes the meaning of a program/model by specifying how it executes on an abstract machine; 2) denotational semantics which uses precise mathematical concepts to define the meaning of a program/model; 3) axiomatic semantics which tries to define the meaning of a program/model by giving proof rules for it within a program logic. Example semantics will be covered for each semantic model.
The course combines theory and practice. The course discusses issues on semantic models, and their relations with logical program/model reasoning, e.g., theorem proving, model checking.