|
Tag: Redirect target changed |
| (One intermediate revision by the same user not shown) |
| Line 1: |
Line 1: |
| | | #redirect [[Some abstractions around programming#Invariants]] |
| ===In math===
| |
| <!--
| |
| In math, invariants are mostly used to point out the concept of 'something that remains unchanged under certain transformations'
| |
| | |
| In particular being able to say that something holds under entire ''classes'' of transformations.
| |
| | |
| | |
| This is potentially useful to
| |
| * classify mathematical objects
| |
| | |
| * characterize certain objects.
| |
| : say, the Pythagorean theorem is an an invariant property of right triangles
| |
| :: (and is still invariant under any operation that maintains the property of being a right triangle)
| |
| : going a little further, {{search|Fundamental invariants of triangles}}
| |
| | |
| | |
| * mention what to watch out for in more pragmatic use
| |
| : Say, programmers (around graphics, geography, and more) may care to know things like
| |
| :: the area of a triangle is invariant under translation, rotation and reflection, but not under magnification.
| |
| :: angles are invariant under all of those
| |
| | |
| * It is sometimes useful to explain the contraints of a given problem or puzzle.
| |
| | |
| * It's useful around various topology.
| |
| | |
| * It'll also easily turn up around [[symmetries]]. And [[fractals]].
| |
| | |
| | |
| https://mathworld.wolfram.com/Invariant.html
| |
| | |
| -->
| |
| | |
| ===In more practical engineering===
| |
| <!--
| |
| In pragmatic terms, invariants are related to the assumpption we're making.
| |
| | |
| For example, in 3D sensing, it can be useful to point out you are assuming detection is more or less invariant with direction.
| |
| | |
| Particularly when you ''know'' this isn't true, to point out that you know - and that it works well enough, and things stay a lot simpler, if you ''do'' make that assumption.
| |
| -->
| |
| | |
| | |
| ===In programming===
| |
| <!--
| |
| Invariants are expressions that does not change in value.
| |
| | |
| Often a boolean expression that should stay true, and often an equality expression.
| |
| | |
| | |
| If the invariant changes, then the code is probably wrong.
| |
| | |
| | |
| Invariants are useful to
| |
| describe behaviour in broad terms,
| |
| describe the correctness of individual operations,
| |
| to test these,
| |
| and to do that while debugging.
| |
| | |
| | |
| | |
| | |
| | |
| Uses
| |
| * invariants are often placed in [[assert]] statements
| |
| :: particularly in the more critical state management, that should halt a program if any mistakes are suspected
| |
| | |
| * presumed-to-be-invariant(-and-suspected-not-to-be) expressions are rather useful to plug into a debugger, to have it alert you when it does change ([[watch expressions]])
| |
| | |
| * invariants have some uses around [[testing]], but in that context often mean 'tests but not very often at all' - checking at just a few points may not be thorough enough.
| |
| | |
| | |
| * invariants can be useful to communicate some agreement
| |
| :: if you know code may rely on some property, or (need to) worry about its absence
| |
| :: then you want to strongly guarantee that (rather than agree that yeah, that's usually true).
| |
| :: even if this is only useful if e.g. documentation tells them
| |
| :: e.g. a rational-number class could ensire the denominator is never zero, so only that class and no ''other'' code ever has to edge-case for that
| |
| | |
| | |
| * sometimes much less formal, just a way of reasoning about what the object should be doing.
| |
| | |
| * there are further qualifiers you could add to the word invariant. For example, [https://course.ccs.neu.edu/cs3500sp16/lec_07_notes.html this page] argues a heap can be said to have
| |
| ** the ''logical invariant'' that is the heap-ordering property
| |
| ** the ''structural invariant'' that keeps a tree as short as it could be, basically O(log n) deep for n items{{verify}}
| |
| | |
| | |
| | |
| | |
| | |
| '''Invariants and execution threads'''
| |
| | |
| | |
| It is often assumed the invariant may temporarily not hold during said work, but will afterwards.
| |
| | |
| In the basic case, you could invariants e.g. at the start and end of a unit of work, like a function.
| |
| | |
| | |
| ...which is fine when that unit of work acts atomic in execution, yet things like pre-emptive multitasking can break that assumption completely.
| |
| | |
| Which makes invariants additionally useful to detect the possibility or clear presence of race conditions, or other sort of unsafe code.
| |
| | |
| | |
| For example, semaphores have an invariant that their correct behaviour depends on.
| |
| | |
| Semaphore implementations must make a few of its operations act atomically to ensure this.
| |
| | |
| {{comment|(with S being the semaphore value and S<sub>0</sub> the initial value, the invariant expression is something like
| |
| <tt>S==S<sub>0</sub>+ExecutedSignals-CompletedWaits</tt>)}}.
| |
| | |
| | |
| | |
| Note that without parallelism, invariants checking at the start and end of a function is often enough, simply because there is no possible interruption of this thread of execution.
| |
| | |
| This also holds under non-parallel, cooperative multitasking.
| |
| | |
| With parallelism like pre-emptive multitasking, you cannot know when it switches tasks, so the invariant must now basically hold ''at all times'', which is much harder.
| |
| | |
| For example, when you're checking whether you have enough locking, you could say that any code that can read the relevant variables should see the state as the invariant says at ''all'' times.
| |
| | |
| This is part of why it's so easy to do something wrong in bare multithreading code, and one of the reasons people like cooperative multitasking when its other shortcomings are fine in the context.
| |
| | |
| -->
| |
| | |
| ====Class invariant====
| |
| <!--
| |
| | |
| | |
| | |
| A [[class invariant]], also known as '''type invariant''' (and apparently '''object invariant'''{{verify}}) is something that should stay true throughout an object's lifetime, regardless of its state.
| |
| | |
| | |
| This isn't any different from the above concept, just points out you can often think of an object as a sort of state machine that you may change on any call.
| |
| | |
| | |
| | |
| -->
| |
| | |
| [[Category:Programming]]
| |