Primitive recursive functions and fixpoints

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

Endofunctions, closures, cycles and chains

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

Mutable structures: Arrays

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

Introduction to processes

Basics A function is a computation object which calculates a result given its arguments. A procedure is a computation object which establishes a postcondition provided that its precondition is satisfied. Functions and procedures do not interact with their environment during their lifetime. They just have an entry point and an exit point. What happens between […]

Closures and fixpoints

Introduction Recursive definitions of functions (and processes as we well see later) are fixpoint equations. The simple example of the recursive definiton of the factorial function can be used to illustrate this fact. fact(n:NATURAL): NATURAL ensure Result = if n=0 then 1 else n*fact(n-1) end end This definition is equivalent to the following assertion. fact_all: […]

Functions and Complete Partial Orders

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

Binary Relations, Endorelations and Transitive Closures

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