Several examples are given for the design of programming language semantics as well as model-checking and program analysis algorithms. To illustrate the notions of relative completeness and of existence of a best abstraction, we show that transitional, demonic, natural and angelic denotational, predicate transformer and axiomatic semantics are all relatively complete, best abstractions of a maximal trace semantics (or equivalently that the maximal trace semantics is a refinement of all these semantics). To illustrate incompleteness, we consider model-checking of finite transition systems for a temporal logic, both with maximal trace semantics. The logic can be restricted to ensure relative completeness at the expense of expressiveness. To illustrate inexistence of best approximations, we consider several abstract domains for the abstraction of sets of vectors of numbers and sets of graphs (for so-called set-based analysis).
Monday, 07-May-2012 17:51:05 EDT