Invariant based programming

Invariant based programming

Invariant based programming is a programming methodology where specifications and invariants are written before the actual program statements. Writing down the invariants during the programming process has a number of advantages: it requires the programmer to make his intentions about the program behavior explicit before actually implementing it, and invariants can be evaluated dynamically during execution to catch common programming errors. Furthermore, if strong enough, invariants can be used to prove the correctness of the program based on the formal semantics of program statements. A combined programming and specification language, connected to a powerful formal proof system, will generally be required for full verification of non-trivial programs. In this case a high degree of automation of proofs is also possible.

In most existing programming languages the main organizing structures are control flow blocks such as for loops, while loops and if statements. Such languages may not be ideal for invariants-first programming, since they force the programmer to make decisions about control flow before writing the invariants. Furthermore, most programming languages do not have good support for writing specifications and invariants, since they lack quantifier operators and one can typically not express higher order properties.

The idea of developing the program together with its proof originated from E.W. Dijkstra. Actually writing invariants before program statements has been considered in a number of different forms by M.H. van Emden, J.C. Reynolds and R-J Back.

See also

Eiffel (programming language)


Wikimedia Foundation. 2010.

Игры ⚽ Поможем решить контрольную работу

Look at other dictionaries:

  • Programming language — lists Alphabetical Categorical Chronological Generational A programming language is an artificial language designed to communicate instructions to a machine, particularly a computer. Programming languages can be used to create programs that… …   Wikipedia

  • Eiffel (programming language) — Infobox programming language name = Eiffel paradigm = object oriented year = 1986 designer = Bertrand Meyer developer = Bertrand Meyer Eiffel Software latest release version = 4.2 latest release date = Feb 6, 1998 typing = static typing, strong… …   Wikipedia

  • Dynamic programming — For the programming paradigm, see Dynamic programming language. In mathematics and computer science, dynamic programming is a method for solving complex problems by breaking them down into simpler subproblems. It is applicable to problems… …   Wikipedia

  • SAC programming language — Infobox programming language name = SAC paradigm = array, functional year = 1994 designer = Sven Bodo Scholz, Clemens Grelck, et al developer = latest release version = latest release date = typing = static, strong implementations = dialects =… …   Wikipedia

  • Class (computer science) — In object oriented programming, a class is a programming language construct that is used as a blueprint to create objects. This blueprint includes attributes and methods that the created objects all share.More technically, a class is a cohesive… …   Wikipedia

  • Software transactional memory — In computer science, software transactional memory (STM) is a concurrency control mechanism analogous to database transactions for controlling access to shared memory in concurrent computing. It is an alternative to lock based synchronization. A… …   Wikipedia

  • Crawljax — is a free and open source web crawler for automatically crawling and testing modern Ajax based Web applications. Crawljax was originally developed by Ali Mesbah and Arie van Deursen as part of a PhD project.[1][2][3] Later on it was extended by… …   Wikipedia

  • Domain-specific language — Programming paradigms Agent oriented Automata based Component based Flow based Pipelined Concatenative Concurrent computing …   Wikipedia

  • Cellular neural network — Cellular neural networks (CNN) are a parallel computing paradigm similar to neural networks, with the difference that communication is allowed between neighbouring units only. Typical applications include image processing, analyzing 3D surfaces,… …   Wikipedia

  • List of important publications in computer science — This is a list of important publications in computer science, organized by field. Some reasons why a particular publication might be regarded as important: Topic creator – A publication that created a new topic Breakthrough – A publication that… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”