One post tagged with "specification"

In OCaml, we create a compare function for many data structures to have:

• an ordering, and:
• an equality function.

These compare functions should behave as follows:

• compare x y returns -1 when x is "lesser" than y;
• compare x y returns 0 when x is "equal" to y;
• compare x y returns 1 when x is "greater" than y.

The compare functions are useful to implement many algorithms and derive data structures such as maps and sets. Having an issue in the consistency of such functions can lead to bugs in the code using them. An example of inconsistency is to have both:

• compare x y = 1 and:
• compare y x = 1

for some values of x and y. A complex example of compare function in the code of Tezos is located in the Script_comparable.v file to compare arbitrary Michelson values.

In this blog post we will see how we specify the compare functions and verify them.