Content deleted Content added
→Notes: Rename section to "References" |
Added short description Tags: Mobile edit Mobile app edit Android app edit App suggested edit App description add |
||
Line 1:
{{Short description|Methodology of programming}}
'''Invariant-based programming'''<ref>Back, Ralph-Johan: [https://hal.archives-ouvertes.fr/hal-00477903/document Invariant Based Programming: Basic approach and Teaching Experience], Formal Aspects of Computing, 14 February 2008, ISSN 0934-5043 (Print) 1433-299X (Online)</ref> is a programming methodology where [[Formal specification|specifications]] and [[Invariant (computer science)|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 their 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 [[Formal verification|correctness]] of the program based on the [[Formal semantics of programming languages|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.
| |||