Order structures: An excercise in abstraction and multiple inheritance

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” […]

Predicates, ghost predicates and higher order predicates

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 […]

Proofs made easy with proof procedures

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++, […]