RELATIONAL MODEL FOR PROGRAM SEMANTICS
Pradeep Kumar Punnam · OhioLink ETD Center (Ohio Library and Information Network) · 2008
Extensive research is going on in proving equivalences between different methodologies of specifying the semantics.C.A.R.Hoare et al. [1] tried to show how algebraic style of semantics can be used to derive operational semantics.And Robin Milner [2] showed how we can use operational semantics to get algebraic semantics.We believe that the relational model is perfectly suited to prove the equivalence between different semantics.We define refinement and step relations on programs to give an operational semantics view using relations.Modeling non-determinism has been a difficult problem for long time, and traditional semantic methodologies are not suitable in specifying and understanding their properties.Different semantics used special notations to represent non determinism.But relations intuitively model non-determinism in them selves.Relations enable us to better describe and understand the non-deterministic properties of the language.K. Rustan M.Leino et al.[3] presents a way of reasoning about the secure information flow using the weakest precondition calculus and relations.Relational model with operational view will give us better understanding of the informational flow to reason about the security in programs.In the following chapter we are going to introduce some of the background concepts on relations, and in chapter 3 we are going to present introductions on syntax, semantics and three semantic methodologies (axiomatic, denotational and operational semantics).We will introduce the relational model in the chapter 4 by defining variables, states and programs, and provide some of the properties using Hoare and Smyth orderings.We also present some of the primitives and properties of programming languages given by Hoare et al., and prove them in the relational model.At the end we define refinement and non-determinism and provide properties using the relational model.CHAPTER 2 Background Concepts Set TheoryA set can be viewed as a collection of objects, the elements or members of the set.We write a ∈ X when a is an element of the set X. Types of sets:Empty Set: A set which has no elements is called the empty set.More formally, the empty set, denoted by ∅, is a set that satisfies the following: ∀x x / ∈ ∅. Universal Set:A set which has all the elements in the universe of discourse is called a universal set.More formally, a universal set, denoted by U , is a set that satisfies the following: ∀x x ∈ U .Equality of sets: Two sets are equal if and only if they have the same elements.More formally, for any sets A and B, A = B if and only if ∀x[x ∈ A ←→ x ∈ B]. Constructions on sets :A new set can be constructed from two or more sets using the following operations.