Proving Invariants of Functional Programs.
Zoltán Horváth, Tamás Kozsik, Máté Tejfel · 2003
In a pure functional language like Clean the values of the functional variables are constants; variables of functional programs do not change in time. Hence it seems that temporality has no meaning in functional programs. However, in certain cases (e.g. in interactive or distributed programs, or in ones that use IO) we would like to consider a series of values computed from each other as different states of the same “abstract object”. For this abstract object we can already prove temporal properties. In this paper we present the concept of object abstraction and show how to interpret and prove temporal properties of functional programs.