2.7 KiB
| title | chunk | source | category | tags | date_saved | instance |
|---|---|---|---|---|---|---|
| Invariant (mathematics) | 3/3 | https://en.wikipedia.org/wiki/Invariant_(mathematics) | reference | science, encyclopedia | 2026-05-05T07:24:05.176600+00:00 | kb-cron |
=== Unchanged under perturbation === Thirdly, if one is studying an object that varies in a family, as is common in algebraic geometry and differential geometry, one may ask if the property is unchanged under perturbation (for example, if an object is constant on families or invariant under change of metric).
== Invariants in computer science ==
In computer science, an invariant is a logical assertion that is always held to be true during a certain phase of execution of a computer program. For example, a loop invariant is a condition that is true at the beginning and the end of every iteration of a loop. Invariants are especially useful when reasoning about the correctness of a computer program. The theory of optimizing compilers, the methodology of design by contract, and formal methods for determining program correctness, all rely heavily on invariants. Programmers often use assertions in their code to make invariants explicit. Some object oriented programming languages have a special syntax for specifying class invariants.
=== Automatic invariant detection in imperative programs === Abstract interpretation tools can compute simple invariants of given imperative computer programs. The kinds of properties that can be found depend on the abstract domains used. Typical example properties are single integer variable ranges like 0<=x<1024, relations between several variables like 0<=i-j<2*n-1, and modulus information like y%4==0. Academic research prototypes also consider simple properties of pointer structures. More sophisticated invariants generally have to be provided manually. In particular, when verifying an imperative program using Hoare logic, a loop invariant has to be provided manually for each loop in the program, which is one of the reasons that this approach is generally impractical for most programs. In the context of the above MU puzzle example, there is currently no general automated tool that can detect that a derivation from MI to MU is impossible using only the rules 1–4. However, once the abstraction from the string to the number of its "I"s has been made by hand, leading, for example, to the following C program, an abstract interpretation tool will be able to detect that ICount%3 cannot be 0, and hence the "while"-loop will never terminate.
== See also ==
== Notes ==
== References ==
== External links == "Applet: Visual Invariants in Sorting Algorithms" Archived 2022-02-24 at the Wayback Machine by William Braynen in 1997