### Primitive recursive functions and fixpoints

Posted by helmutbrandl in Uncategorized on April 29, 2013

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

Posted by helmutbrandl in Uncategorized on March 18, 2013

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

Posted by helmutbrandl in Uncategorized on February 4, 2013

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

Posted by helmutbrandl in Uncategorized on December 3, 2012

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

Posted by helmutbrandl in Uncategorized on November 28, 2012

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

Posted by helmutbrandl in Uncategorized on November 19, 2012

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

Posted by helmutbrandl in Uncategorized on October 18, 2012

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