Function contracts allow for input- and output parameters, in this case a fractional permission. The `drop` function takes as input a fractional permission `p` and gives as output a fractional permission `q` that is at most `p` (so that `q <= p`). This verification example shows how to handle such input/output parameters.
Path to example file
Lines of code
18 lines (comments not included)
Lines of specification
4 lines (22.22% of the total)
Note, verification may take a while and has a time-out of 20 seconds.