Geek Answers Handbook

Mathematical notation of programming concepts

There are many methods for representing the structure of a program (for example, UML class diagrams, etc.). I am wondering if there is a convention that describes programs in a rigorous, mathematical way. I am particularly interested in using mathematical notation for this purpose.

Example : classes are represented as sets (fields, properties) and functions (working on elements of sets). The fields of the parent class are a subset of the child class. The functions are described in pseudocode, which should look like this ...

+4
source share
10 answers

I know that Z Notation is used to some extent in formal verification of software, for example, the Tokeneer project .

Z notation

Z Reference Guide

+2
source

Yes, there is Floyd-Hoare Logic .

+1
source

There are many ways, but I think that most of them are inconvenient for expressing structure, since structure is often not expressed in mathematical mathematical standards by default. The main exception is, of course, functional programming languages. Think of folds (catamorphism), groups, algebra, etc.

For imperative programming, I know about the existence of Z, which uses (pure and extended) set theory of lambda calculi and (first-order predicate logic). However, I do not think it is very convenient. The only potential use of mathematics to express structure is the fact that you can prove it. But if you want to do this, take a look at JML, SpeC # or Eiffel.

+1
source

Depending on what you are trying to do, but going down this road with specific languages ​​can lead to trouble.

For example, see the discussion of round ellipses in the C ++ FAQ Lite.

+1
source

This book uses the deductive method of programming through affiliate programs with abstract mathematical theory that allow them to work. [...]

I believe that the "Programming Elements" by Alexander Stepanov and Paul MacJon are pretty close to what you are looking for.

Concepts

A concept is a description of the requirements for one or more types described in terms of the existence and properties of procedures, type attributes and type functions by types.

+1
source

Z, which has already been mentioned, is pretty much what you are describing. There are several options for this for object-oriented modeling, but I think you can go pretty far from "standard Z-schemes" if you want to model classes.

There's also Alloy , which is newer and more inspired by Z. Its designation is perhaps a little closer to object orientation. It is also analyzed, i.e. You can check the models you created regardless of whether they fulfill certain conditions, but cannot prove that the properties are preserved, just try to refute within the final area.

A reliable design software article is a great introduction to Alloy and its counterparts, as well as a table of available similar tools.

+1
source

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

+1
source

There is a mathematical language that actually describes a program, or rather, its operations. You take the initial state, and then transform this state until you reach the desired target state. Conversions give the program code that must be executed.

See the Wikipedia article on Hoar logic .

The basic idea is that for each function (regardless of whether you put it in a class or in an old-style function), you have a pre-condition and a post-condition. For example, a precondition may be that you have an array with >= 0 elements. The post-condition is that each element [i] must be equal to <= element [j] for each i <= j.

The usual description would be "function sorts array". But mathematical terms allow you to convert an input (which must correspond to a precondition) into output (which must correspond to a postcondition).

This is a bit cumbersome to use, especially for more complex programs, but some of the examples are pretty impressive. Often you get really compact code as a result, which looks rather complicated, but works on the first try.

0
source

I would suggest a programming algebra. This is a computational approach to programs using Relational Algebra , and Galois Connections .

If you still have interest in this topic, you can find a wonderful article here , Shin-Cheng Mu and Jose Nuno Oliveira ( slides ).

The use of relational algebra and first-order logic also goes well with Alloy , functional programming, and contract design (easily applied to object-oriented programming).

0
source

More articles:


All Articles