vault backup: 2023-10-04 11:39:53
This commit is contained in:
parent
ce92b78c09
commit
40db9d7ce2
@ -1,6 +1,6 @@
|
|||||||
An abstract type have a signature, which contains types, uses and operations, and have some axioms.
|
An abstract type have a signature, which contains types, uses and operations, and have some axioms.
|
||||||
|
|
||||||
An axiom let us determine the value of the application of the observers with the internal operations (in the example below, the operation modify). We can see that as a validation. An axiom must be precise.
|
An axiom let us determine the value of the application of the observers with the internal operations (in the example below, the operation modify). We can see that as a validation. An axiom must be precise. An axiom is the application of the observer on an internal operation : `observer(internal operation)`
|
||||||
|
|
||||||
```
|
```
|
||||||
Types
|
Types
|
||||||
@ -17,3 +17,4 @@ Axioms
|
|||||||
lowerlimit(v) =< i =< upperlimit(v) -> nth(modify(v,i,e), i) = e
|
lowerlimit(v) =< i =< upperlimit(v) -> nth(modify(v,i,e), i) = e
|
||||||
```
|
```
|
||||||
In this example, the axiom explain that it check nth position in the modified vector
|
In this example, the axiom explain that it check nth position in the modified vector
|
||||||
|
|
Loading…
x
Reference in New Issue
Block a user