Mathematical notation of programming concepts

Question

There are many methods for representing structure of a program (like UML class diagrams etc.). I am interested if there is a convention which describes programs in a strict, mathematical way. I am especially interested in the use of mathematical notation for this purpose.

An example: Classes are represented as sets (fields, properties) and functions (operating on the elements of sets). A parent class' fields are a subset of child class'. Functions are described in pseudocode which has to look like this and that...

Answer 1

Yes, there is, Floyd-Hoare Logic.

Answer 2

There are a lot of way, but i think most of them are inconvenient for expressing the structure since the structure is often not expressable in default mathematical concepts. The main exception is of course functional programing languages. Think about folds (catamorphisme), groups, algebra's etc.

For imperative programming I know of the existence of Z, which uses (pure and extended) lambda calculus set theory and (first order) predicate logic. However, i dont think it's very convenient. The only upside of using mathematics to express structure is the fact that you can prove stuff about it. But if you want to do that, take a look at JML, Spec# or Eiffel.

Answer 3

Depends on what you're trying to accomplish, but going down this road with specific languages can get you into trouble.

For example, see the circle-ellipse discussion on C++ FAQ Lite.

Answer 4

I know that Z Notation has been used to some extent in the formal verification of software, such as the Tokeneer project.

Z Notation

Z Reference Manual

Answer 5

This book applies the deductive method to programming by affiliating programs with the abstract mathematical theories that enable them work. [...]

I believe that Elements of Programming by Alexander Stepanov and Paul McJones, is pretty close to what you are looking for.

Concepts

A concept is a description of requirements on one or more types stated in terms of the existence and properties of procedures, type attributes, and type functions defined on the types.

Answer 6

There is a mathematical language which actually describes a program or rather it's operations. You take the initial state and then transform this state until you reach the desired target state. The transformations yield the program code which must be executed.

See the Wikipedia article about Hoare logic.

The basic idea is that for every function (no matter if you put that into a class or into an old style function), you have a pre- and a post-condition. For example, the precondition can be that you have an array which has >= 0 elements. the post-condition is that every element[i] must by <= element[j] for every i <= j.

The usual description would be "the function sorts the array". But the mathematical terms allow you to transform the input (which must match the precondition) into the output (which must match the postcondition).

It's a bit unwieldy to use, especially for more complex programs but some of the examples are pretty impressive. Often, you get really compact code as the result which looks quite complex but works at first try.

Answer 7

http://www.amazon.com/Concrete-Mathematics-Foundation-Computer-Science/dp/0201558025

Answer 8

Z, which has already been mentioned, is pretty much what you describe. There are some variants of it for object-oriented modelling, but I think you can get quite far with "standard Z's" schemas if you wish to model classes.

There's also Alloy, which is newer and inspired by Z. Its notation is perhaps a bit closer to object-orientation. It is also analysable, i.e. you can check the models you create whether they fulfill certain conditions, but it cannot prove that properties hold, just attempt to refute within a finite scope.

The article Dependable Software by Design is a nice introduction to Alloy and its ilk, along with a table of available similar tools.

Answer 9

You are looking for functional programming. There are several functional programming languages, and they are all based on a fundamental mathematical theory called the Lambda calculus. Programs written in a functional programming language such as LISP are a mathematical representation of themselves. ;-)