An entrypoint's postcondition says what the execution of the entrypoint changes in the contract storage when it does not fail.
Say the contract storage is made of S items (int, string, map, list, ...) and that the contract code is made of E entrypoints. There is S postconditions to describe the effect of one entrpoint on the S storage items, which is a total number of postconditions of E * S for the entire contract.
Consider the basic contract with one storage item
value and one entrypoint
There needs only one postcondition to describe the effect of the entrypoint on the storage:
If the entrypoint can only be called by the
owner address, the postcondition becomes:
The form of the postcondition above is:
which reads If
CONDITION holds, then
CHANGE occurs, or
When an entrypoint does not change a storage item, it is stated with the following postcondition:
The prefix keyword
before is used to refer to the state of the storage item
ITEM before entrypoint execution. The storage item without prefix refers to the storage item after entrypoint execution.
For example, below is the postcondition for the entrypoint
transfer of the FA 1.2 fungible token contract regarding the
ledger storage item. It states that this storage item does not change if the parameter address
%from is equal to the parameter address
The postcondition is not trivial since the code explicitely states how it changes the
ledger asset, as highlighted in the code above. However, if
%to, then there is no final change in the
ledger item since
value is subtracted and then added back to the address entry.
To be complete, the postcondition above must say what changes when
%from is different from
A general form of the postcondition is actually:
where conditions 1 to n are such that they cover all branches of execution. More formally, conditions are such that the following statement is true:
The postcondition for the
tranfer entrypoint regarding the
ledger item is then:
Note that it is equivalent either to declare one postcondition formed as the conjunction of n implication statements, or to declare n postconditions of the form of an implication:
is equivalent to:
The later form is preferred since it attributes an id to each implication statement, making the output from the formal system in charge of proving them more explicit.
This section deals with collections of pairs of key and value. Archetype provides 3 types of collections: Michelson map and big_map, and asset used in examples below.
Conversly to code language, retrieving an asset with key
k from an asset collection
c does not fail and the non existence is managed with the keyword
When an object
a with known id
k in a collection
c is changed, the postcondition has the following structure:
ais the object associated to
kafter entrypoint execution
bais the object associated to
CHANGEis the change in object a statement
NOTEXISTkBEFOREis the statement when
adoes not exist before
NOTEXISTkAFTERis the statement when
adoes not exist after
For example, below is the postcondition
p3_approve for the entrypoint
approve of the FA 1.2 fungible token contract regarding the
allowance asset with key
(caller,spender). It corresponds to the
addupdate code instruction.
false statement means there is a logical contradiction. In the case above, it is not possible that the object with key
(caller,spender) does not exist, as it is the semantic of the
addupdate instruction (see code above in 'entrypoint' tab).
otherwise statements are presented below for instructions
Postconditions say which objects are not changed with a statement of the following form:
CHANGED is the statement to say that object
a is not a changed object.
When object with key
k is the only object changed, the postcondition is:
KEY is the key field of the asset.
When changed objects are not known by their ids, but rather by a business rule based on object data, the goal is to state the effect of the change on the collection.
For example, below is the postcondition
p2 for the entrypoint
consume of the Miles contract. It states that the entrypoint reduces by parameter value
quantity the total number of miles, which is the business intent of the entrypoint:
The total number of miles is obtained by summing the field
amount because miles are stored per bunch associated to an expiration date.
Note that in this case, it is more complex to state exactly which miles are changed or not changed, as it is the result of an iteration process over a sorted and filtered set of miles.
It is interesting though to make sure that only not expired miles are consumed (removed), since it is another key functional element of the contract:
Note that Archetype specification language provides convenient handlers for removed or added assets. Another way to phrase this property is: