Verifiable Software

Introduction Recursion and fixpoint equations The mathematical content of the definition of a recursive function is a fixpoint equation. Let us demonstrate this statement with a simple example. The textbook example of a recursive function is the factorial function. In our programming language it looks like factorial(n:NATURAL): NATURAL ensure Result = if n=0 then 1 […]

Introduction Motivation Endofunctions are functions f of type A->A where A can be any type. Since all functions are partial functions we can use endofunctions to model linked structures. E.g. if we have an object which has an optional reference to an object of the same type the optional reference can be viewed as a […]

Introduction Nearly all languages with imperative elements have some kind of an array. In C an array is just a typed pointer to a memory region. You can address the different elements by giving an offset to the start of the memory region. The compiler multiplies the offset with the size of the objects contained […]

Motivation Why study complete partial orders? Let us look at some simple examples. Everybody knows the recursive definition of the factorial function. In our programming language the definition looks like: factorial(n:NATURAL): NATURAL ensure Result = if n=0 then 1 else n*factorial(n-1) end end But this is not a classical definition. A classical definition of a […]

Introduction Relations are an important vehicle to write specifications. In this article we study some properties of binary relations. First we start from binary relations in general with domain, range, composition, images etc. In the second part we study endorelations i.e. binary relations where the type of the domain and the range are the same. […]

Mathematical sets Sets abound in mathematics. If a mathematician wants to treat a collection of objects which satisfy a certain property as an entity, he defines a set. Sets are a very powerful tool in specifications. In order to obtain good readability we introduce a set like notation. Set expressions The expression {1,2,3} is the […]

Introduction This article is dedicated to boolean lattices. A boolean lattice is another name for a boolean algebra. A boolean lattice is an algebraic structure with two binary operators “*” and “+” which represent “and” and “or”, a unary operator “-” which represents negation. The binary operators are commutative, associative and distributive. Furthermore there are […]

Introduction Types which satisfy the concept of a partial order (i.e. which are descendants of the type PARTIAL_ORDER) have a binary relation “<=” which is reflexive, transitive and antisymmetric, i.e. for every three objects “a”, “b”, and “c” the following conditions are satisfied: reflexive: a<=a transitive: a<=b => b=>c => a=>c antisymmetric: a<=b => b=>a […]

Introduction Insertion sort is one of the simplest sorting algorithms. It is quite efficient for small arrays. Its runtime increases with the square of the number of elements to be sorted. Therefore it should not be used with large data sets. For large data sets algorithms like merge sort or heap sort are far more […]

The specification In the previous article the specification of a buffer of elements of a certain type has been described. Let us repeat here shortly the essence of the specification. class BUFFER[G] feature capacity: NATURAL content: ghost LIST[G] count: NATURAL ensure Result = content.count end [] (i:NATURAL): G require i < count ensure Result ~ […]

Basics Modern Eiffel has immutable and mutable types. An object of immutable type cannot be modified, an object of mutable type can be modified. Therefore we say that an object is mutable or immutable depending on its type. Immutable objects don’t have an own identity. The identity of an immutable object is completely determined by […]

Introduction Order structures seem to be abstract concepts of theoretical mathematics with minor practical importance. But this is just at first glance. A closer look reveals that many data types have order structure. – The basic types NATURAL, INTEGER, FLOAT etc. have a total order – The type SET[T] has a partial order with “is_subset” […]

Motivation Predicates play an important role in specifying functions and procedures. Since predicates are mainly used within assertions (i.e. within contracts) it is often not necessary that predicates are computable. We often use predicates to express not computable properties and give them a concise name instead of repeating a long and clumsy boolean expression over […]

Introduction The Modern Eiffel project has two major goals: Design and implement a language which (a) allows formal verification and (b) is usuable by programmers. The second goal has not yet been fully met, because the interface to the proof engine is not easy to grasp for prgrammers coming from object oriented languages like C++, […]

Ghost functions Boolean expressions of the form all(x:X) p(a,x) — x is a bound variable, a is free within the expression some(x:X) p(a,x) are not computable in general, even if the boolean valued function “p” is computable. I.e. the following constructs are illegal in executable code. — Illegal if expression!!! if all(x:X) p(a,x) then exp1 […]

Introduction Tuples are very versatile in Modern Eiffel. This is due to the possibility that tuples and sequences of expressions can be freely mixed as long as the corresponding types match. In the following tuples and the possible use of tuples in expressions and functions is shown. Tuples Tuples are product types. If you have […]