Project topics and materials
Get Complete Project Material File(s) Now! »
Basic Notions and Notations
In the following, we briefly recall well-known mathematical concepts in order to establish the notation used throughout this thesis.
Sets. A set S is defined as an unordered collection of distinct elements. We write s 2 S (resp. s 62S) when s is (resp. is not) an element of the set S. A set is expressed in extension when it is uniquely identified by its elements: we write {a, b, c} for the set of elements a, b and c. The empty set is denoted by ;. A set is expressed in comprehension when its elements are specified through a shared property: we write {x 2 S | P (x)} for the set of elements x of the set S for which P (x) is true. The cardinality of a set S is denoted by |S|.
A set S is a subset of a set S0, written S ✓ S0, if and only if every element of S is an element of S def 0. The empty set is a subset of every set. The power set P(S) of a set S is the set of all its subsets: P(S) = {S0 | S0 ✓ S}. and B , written A [ B , is the set of all elements of A
The union of two sets A def | and all elements of B : A [ B = { x x 2 A _ x 2 B} . More generally, the union A \ B S AS BS of a set of sets S, is denoted by S def S02S S0 = {x | 9S0 2 S : x 2 S0}. : S
The intersection of two sets def and is the set of all elements that are elements of both A and B: A \ B {x | x 2 A ^ x 2 B}. More generally, the intersection of a set of sets S is denoted by T S: S def S02S S0 = = {x | 8S0 2 S : x 2 S0}. The relative T B T A , complement of a set in a set denoted by , is the set of all elements of A that are not elements of defA \ B B: A\B = {x | x 2 A ^ x 62B}. When B ✓ A and the set A is clear from the context, we simply write ¬B for A \ B and we call it complement of B. The cartesian product of two sets A and B, denoted by A ⇥ B, is the set of all pairs where the first component is an element of A and the second : def x, y x y . More component is an element of B A ⇥ B = {h i | 2 A ^ 2 B} def def generally, S1 ⇥ • • • ⇥ Sn = {hx1, . . . , xni | x1 2 S1 ^ • • • ^ xn 2 Sn} and Sn = {hx1, . . . , xni | x1 2 S ^ • • • ^ xn 2 S} is the set of n-tuples of elements of S.
A covering of a set S is a set P of non-empty subsets of S such that any element s 2 S belongs to a set in P: S = S P. A partition of a set S is a covering P such that any two sets in P are disjoint, that is, any element s 2 S belongs to a unique set in P: 8X, Y 2 P : X 6= Y ) X \ Y = ;.
Relations. A binary relation R between two sets A and B is a subset of the cartesian product A ⇥ B. We often write x R y for hx, yi 2 R.
The following are some important properties which may hold for a binary relation R over a set S:
8x 2 S : x R x (reflexivity)
8x 2 S : ¬(x R x) (irreflexivity)
8x, y 2 S : x R y ) y R x (symmetry)
8x, y 2 S : x R y ^ y R x ) x = y (anti-symmetry)
8x, y, z 2 S : x R y ^ y R z ) x R z (transitivity)
8x, y 2 S : x R y _ y R x (totality)
An equivalence relation is a binary relation which is reflexive, symmetric, and transitive. A binary relation which is reflexive (resp. irreflexive), anti-symmetric, and transitive is called a partial order (resp. strict partial order ). A preorder is reflexive and transitive, but not necessarily anti-symmetric. A (strict) total order is a (strict) partial order which is total.
Ordered Sets. A partially ordered set or poset (resp. preordered set) hD, vi is a set D equipped with a partial order (resp. preorder) v. A finite partially ordered set hD, vi can be represented by a Hasse diagram such as the one in Figure 2.1: each element x 2 D is uniquely represented by a node of the diagram, and there is an edge from a node x 2 D to a node y 2 D if y covers x, that is, x y and there exists no z 2 D such that x z y. Hasse diagrams are usually drawn placing the elements higher than the elements they cover.
Let hD, vi be a partially ordered set. The least element of the poset, when it exists, is denoted by ?: 8d 2 D : ? v d. Similarly, the greatest element of the poset, when it exists, is denoted by >: 8d 2 D : d v >. Note that any partially ordered set can always be equipped with a least (resp. greatest) element by adding a new element that is smaller (resp. greater) than every other element. Let X ✓ D. A maximal element of X is an element d 2 X such that, for each x 2 X , x v d. When X has a unique maximal element, it is called maximum and it is denoted by max X . Dually, a minimal element of X is an element d 2 X such that, for each x 2 X , d v x. When X has a unique minimal element, it is called minimum and it is denoted by min X . An upper bound of X is an element d 2 D (not necessarily belonging to X ) such that, for each x 2 X , x v d. The least upper bound (or lub, or supremum) of X is an upper bound d 2 D of X and such that, for every upper bound d0 2 D of X , d v d0. When it exists, it is unique and denoted by F X (or sup X ). Dually, a lower bound of X is an element d 2 D such that, for each x 2 X , d v x. The greatest lower bound (or glb, or infimum) of X is a lower bound d 2 D of X such that, for every lower bound d0 2 D of X , d0 v d. When it exists, it is unique and denoted by d X (or inf X ). Note that, the notion of maximal element, maximum, and least upper bound (resp. minimal element, minimum, and greatest lower bound) are di↵erent, as illustrated by the following example.
Example 2.1.1
Let us consider the partially ordered set hP({a, b, c}), ✓i represented in Figure 2.1 and the subset X = {{a}, {b}, {c}, {a, b}, {a, c}, {b, c}}. The maximal elements of X are {a, b}, {a, c}, and {b, c}. Thus the maximum max X of X does not exist, while its least upper bound is sup X = {a, b, c}. Similarly, the minimal elements of X are {a}, {b}, and {c}. Thus, the minimum min X of X does not exist, while its greatest lower bound is inf X.
A set equipped with a total order is a totally ordered set. A totally ordered subset C of a partially ordered set hD, vi is called a chain. A partially ordered set hD, vi satisfies the ascending chain condition (ACC) if and only if any infinite increasing chain x0 v x1 v • • • v xn v • • • of elements of D is not strictly increasing, that is, 9k 0 : 8j k : xk = xj. Dually, a partially ordered set hD, vi satisfies the descending chain condition (DCC) if and only if any infinite decreasing chain x0 w x1 w • • • w xn w • • • of elements of D is not strictly decreasing, that is, 9k 0 : 8j k : xk = xj.
A complete partial order or cpo hD, vi is a poset where every chain C has a least upper bound C, which is called the limit of the chain. Note that, since the empty set ; is a chain, a complete partial order has a least element ? = F ;. Thus, a partially ordered set that satisfies the ascending chain condition and that is equipped with a least element, is a complete partial order.
Lattices. A lattice hD, v, t, ui is a poset where each pair of elements x, y 2 D has a least upper bound, denoted by x t y, and a greatest lower bound, denoted by x u y. Any totally ordered set is a lattice. A complete lattice hD, v, t, u, ?, >i is a lattice where any subset X ✓ D has a least upper bound F greatest lower bound d . A complete lattice has both a least X and adef d D F ; > def F D d ; element ? = and a greatest element .
Example 2.1.2
The power set hP(S), ✓, [, \, ;, Si of any set S is a complete lattice.
Functions. A partial function f from a set A to a set B, written f : A * B, is a binary relation between A and B that pairs each element x 2 A with no more than one element y 2 B. The set of all partial functions from a set A to a set B is denoted by A * B. We write f(x) = y if there exists an element y such that hx, yi 2 f, and we say that f(x) is defined, otherwise we say that f(x) is undefined. Given a partial function f : A * B, we define its domain def as dom(f) = {x 2 A | 9y 2 B : f(x) = y}. The totally undefined function, denoted by ;˙, has the empty set as domain: dom(;˙) = ;. The join of two partial functions f1 : A * B and f2 : A * B with disjoint domains, denoted by f1 [˙ f2 : A * B, is defined as follows:
<>f1(x)
˙ def
f1 [ f2 = x 2 A. f2(x)
:>
where dom(f1) \ dom(f2) = ;.
x 2 dom(f1)
x 2 dom(f2) otherwise
A (total) function f from a set A to a set B, written f : A ! B, is a partial function that pairs each x 2 A with exactly one element y 2 B. Equivalently, a (total) function f : A ! B is a partial function such that dom(f) = A. The set of all functions from a set A to a set B is denoted by A ! B.
We sometimes denote functions using the lambda notation x 2 A. f(x), or more concisely x. f(x).
The composition of two functions f : A ! B and g : B ! C is another function g f : A ! C such that 8x 2 A : (g f)(x) = g(f(x)).
The following properties may hold for a function f : A ! B:
8x, y 2 A : f(x) = f(y) ) x = y (injectivity)
8y 2 B : 9x 2 A : f(x) = y (surjectivity)
A bijective function, also called isomorphism, is both injective and surjective. Two sets A and B are isomorphic if there exists a bijective function f : A !
B. The inverse of a bijective function f : A ! B is the bijective function
f : B ! A defined as f = {hb, ai | ha, bi 2 f}.
Let hD1, v1i and hD2, v2i be partially ordered sets. A function f : D1 ! D2 is said to be monotonic when, for each x, y 2 D1, x v1 y ) f(x) v2 f(y). It is continuous (or Scott-continuous) when it preserves existing least upper bounds of chains, that is, for each chain C ✓ D1, if F C exists then f(F C) = F{f(x) | x 2 C}. Dually, it is co-continuous when it preserves existing greatest lower bounds of chains, that is, if d C exists then f(d C) = d{f(x) | x 2 C}.
A complete t-morphism (resp. complete u-morphism) preserves existing least upper bounds (resp. greatest lower bounds) of arbitrary non-empty sets.
Pointwise Lifting. Given a complete lattice hD, v, t, u, ?, >i (resp. a lat-tice, a cpo, a poset) and a set S, the set S ! D of all functions from S to D inherits the complete lattice (resp. lattice, cpo, poset) structure of D: hS !
D, v˙, t˙, u˙, ?˙, >i˙ where the dotted operators are defined by pointwise lifting:
˙ def
f v g = ˙ def
G˙ X = def
l X˙ = def
Ordinals. The theory of ordinals was introduced by Georg Cantor as the core of his set theory [Can95, Can97].
A binary relation R over a set S is well-founded when every non-empty subset of S has a least element with respect to R. A well-founded total order is called a well-order (or a well-ordering). A well-ordered set hW, i is a set W equipped with a well-ordering . Every well-ordered set is associated with a so-called ordered type. Two well-ordered sets hA, Ai and hB, B i are said to have the same order type if they are order-isomorphic, that is, if there exists a bijective function f : A ! B such that, for all elements x, y 2 A, x A y if and only if f(x) B f(y).
An ordinal is defined as the order type of a well-ordered set and it provides a canonical representative for all well-ordered sets that are order-isomorphic to that well-ordered set. We use lower case Greek letters to denote ordinals. In fact, a well-ordered set h W, i with order type ↵ is order-isomorphic to the well-ordered set {x 2 W | x < ↵} of all ordinals strictly smaller than the ordinal ↵ itself. In particular, as suggested by John von Neumann [vN23], this property permits to define each ordinal as the well-ordered set of all ordinals that precede it: the smallest ordinal is the empty set ;, denoted by 0. The successor of an ordinal ↵ is defined as ↵ [ {↵} and is denoted by ↵ + 1, or equivalently, by succ(↵). Thus, the first successor ordinal is {0}, denoted by 1. The next is {0, 1}, denoted by 2. Continuing in this manner, we obtain all nat-ural numbers, that is, all finite ordinals. A limit ordinal is an ordinal number which is neither 0 nor a successor ordinal. The set N of all natural numbers, denoted by !, is the first limit ordinal and the first transfinite ordinal.
We use hO, i to denote the well-ordered set of ordinals. In the following, we will see that the theory of ordinals is the most general setting for proving program termination.
Fixpoints. Given a partially ordered set hD, vi and a function f : D ! D, a fixpoint of f is an element x
D such that f(x) = x. An element x 2 D
such that x v f(x) is called a pre-fixpoint while, dually, a post-fixpoint is an element x 2 D such that f(x) v x. The least fixpoint of f, written lfp f, is a fixpoint of f such that, for every fixpoint x 2 D of f, lfp f v x. We write lfpd f for the least fixpoint of f which is greater than or equal to an element d 2 D. Dually, we define the greatest fixpoint of f, denoted by gfp f, and the greatest fixpoint of f smaller than or equal to d 2 D, denoted by gfpd f. When the order v is not clear from the context, we explicitly write lfpv f and gfpv f.
We now recall a fundamental theorem due to Alfred Tarski [Tar55]:
Theorem 2.1.3 (Tarski’s Fixpoint Theorem) The set of fixpoints of a monotonic function f : D ! D over a complete lattice is also a complete lattice.
Proof. See [Tar55]. ⌅ d In particular, the theorem guarantees that f has a least fixpoint lfp f = {x 2 D | f(x) v x} and a greatest fixpoint gfp f = F{x 2 D | x v f(x)}.
However, such fixpoint characterizations are not constructive. An alterna-tive constructive characterization is often attributed to Stephen Cole Kleene:
Theorem 2.1.4 (Kleene’s Fixpoint Theorem) Let hD, vi be a complete partial order and let f : D ! D be a Scott-continuous function. Then, f has a least fixpoint which is the least upper bound of the increasing chain
? v f(?) v f(f(?)) v f(f(f(?))) v . . .
i.e., lfp f = F{fn(?) | n 2 N}.
In case of monotonic but not continuous functions, a theorem by Patrick Cousot and Radhia Cousot [CC79] expresses fixpoints as limits of possibly transfinite iteration sequences:
Theorem 2.1.5 Let f : D ! D be a monotonic function over a complete partial order and let d 2 D be a pre-fixpoint. Then, the iteration sequence:
8 d = 0 (zero case)
def < f(f↵) = ↵ + 1 (successor case)
f = :F } otherwise (limit case) > {f↵ | ↵ <
converges towards the least fixpoint lfpd f.
In the following, the partial order between the fixpoint iterates is called computational order, in order to distinguish it from the approximation order defined in the next Section 2.2.2.
Abstract Interpretation
Abstract Interpretation [CC77, Cou78] is a general theory for approximating the semantics of programs, originally developed by Patrick Cousot and Radhia Cousot in the late 1970s, as a unifying framework for static program analysis. In the following, we recall the main definitions and results that will be used throughout this thesis. We refer to [CC92b] for an exhaustive presentation. Transition Systems. The semantics of a program is a mathematical char-acterization of all possible behaviors of the program when executed for all possible input data. In order to be independent from the choice of a particular programming language, programs are often formalized as transition systems:
Definition 2.2.1 (Transition System) A transition system is a pair h⌃, ⌧i where ⌃ is a (potentially infinite) set of states and the transition relation ⌧ ✓ ⌃ ⇥ ⌃ describes the possible transitions between states.
In a labelled transition system h⌃, A, ⌧i, A is a set of actions that are used to label the transitions described by the transition relation ⌧ ✓ ⌃ ⇥ A ⇥ ⌃.
Note that this model allows representing programs with (possibly un-bounded) non-determinism. In the following, in order to lighten the notation, a transition hs, s0i 2 ⌧ (resp. a labelled transition hs, a, s0i 2 ⌧) between a state s and another state s0 is sometimes written as s ! s0 (resp. s a s0).
In some cases, a set I ✓ ⌃ is designated as the set of initial states. The def { 2 | 8 s0 2 h s, s0 i 62}
We define the following functions to manipulate sets of program states.
Definition 2.2.2 Given a transition system h⌃, ⌧i, post : P(⌃) ! P(⌃) maps a set of program states X 2 P(⌃) to the set of their successors with respect to the program transition relation ⌧:
def {s0 2 ⌃ | 9s 2 X : hs, s0i 2 ⌧} (2.2.1)
Definition 2.2.3 Given a transition system h⌃, ⌧i, pre : P(⌃) ! P(⌃) maps a set of program states X 2 P(⌃) to the set of their predecessors with respect to the program transition relation ⌧:
def {s 2 ⌃ | 9s0 2 X : hs, s0i 2 ⌧} (2.2.2)
Definition 2.2.4 Given a transition system h⌃, ⌧i, postg : P(⌃) ! P(⌃) maps a set of states X 2 P(⌃) to the set of states whose successors with respect to the program transition relation ⌧ are all in the set X: post(X) = ⌃ \ post(⌃ \ def { s0 2 ⌃ | 8 s 2 ⌃ : h s, s0 i 2 ⌧ ) s 2 X } (2.2.3)
Definition 2.2.5 Given a transition system h⌃, ⌧i, pref : P(⌃) ! P(⌃) maps a set of states X 2 P(⌃) to the set of states whose predecessors with respect to the program transition relation ⌧ are all in the set X: pre(X) = ⌃ \ pre(⌃ \ def { s 2 ⌃ | 8 s0 2 ⌃ : h s, s0 i 2 ⌧ ) s0 2 X } (2.2.4)
Maximal Trace Semantics
The semantics generated by a transition system is the set of computations described by the transition system. We formally define this notion below.
Sequences. Given a set S, the set Sn def 1 | 8i < n : si 2 S} is = {s0 • • • sn the set of all sequences of exactly n elements from S . We write » to denote 0 def { } the empty sequence, i.e., S » .
Table of contents :
I Introduction
1 Introduction
1.1 Software Verification
1.1.1 Testing
1.1.2 Formal Methods
1.2 Program Properties
1.2.1 Safety Properties
1.2.2 Liveness Properties
1.3 Termination
1.4 Liveness Properties
II Safety
2 Abstract Interpretation
2.1 Basic Notions and Notations
2.2 Abstract Interpretation
2.2.1 Maximal Trace Semantics
2.2.2 Galois Connections
2.2.3 Widening and Narrowing
3 A Small Imperative Language
3.1 A Small Imperative Language
3.2 Maximal Trace Semantics
3.3 Invariance Semantics
3.4 Numerical Abstract Domains
3.4.1 Intervals Abstract Domain
3.4.2 Polyhedra Abstract Domain
3.4.3 Octagons Abstract Domain
III Termination
4 An Abstract Interpretation Framework for Termination
4.1 Ranking Functions
4.2 Termination Semantics
4.2.1 Termination Trace Semantics
4.2.2 Termination Semantics
4.3 Denotational Definite Termination Semantics
5 Piecewise-Defined Ranking Functions
5.1 Piecewise-Defined Ranking Functions
5.2 Decision Trees Abstract Domain
5.2.1 Decision Trees
5.2.2 Binary Operators
5.2.3 Unary Operators
5.2.4 Widening
5.3 Abstract Definite Termination Semantics
5.4 Related Work
6 Ordinal-Valued Ranking Functions
6.1 Ordinal-Valued Ranking Functions
6.2 Ordinal Arithmetic
6.3 Decision Trees Abstract Domain
6.3.1 Decision Trees
6.3.2 Binary Operators
6.3.3 Unary Operators
6.3.4 Widening
6.4 Abstract Definite Termination Semantics
6.5 Related Work
7 Recursive Programs
7.1 A Small Procedural Language
7.2 Maximal Trace Semantics
7.3 Definite Termination Semantics
7.3.1 Definite Termination Semantics
7.3.2 Abstract Definite Termination Semantics
8 Implementation
8.1 FuncTion
8.2 Experimental Evaluation
IV Liveness
9 A Hierarchy of Temporal Properties
9.1 A Hierarchy of Temporal Properties
9.1.1 Safety Properties
9.1.2 Guarantee Properties
9.1.3 Obligation Properties
9.1.4 Recurrence Properties
9.1.5 Persistence Properties
9.1.6 Reactivity Properties
9.2 Guarantee Semantics
9.2.1 Guarantee Semantics
9.2.2 Denotational Guarantee Semantics
9.2.3 Abstract Guarantee Semantics
9.3 Recurrence Semantics
9.3.1 Recurrence Semantics
9.3.2 Denotational Recurrence Semantics
9.3.3 Abstract Recurrence Semantics
9.4 Implementation
9.5 Related Work
V Conclusion
10 Future Directions
Bibliography
A Proofs
A.1 Missing Proofs from Chapter 1
A.2 Missing Proofs from Chapter 4
A.3 Missing Proofs from Chapter 5
A.4 Missing Proofs from Chapter 6
A.5 Missing Proofs from Chapter 7
A.6 Missing Proofs from Chapter 9
