Input/output parameters (succeeding)

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.

General information

ID99
Articlenone
Back-endSilicon
LanguagePVL
Features
Sources
Path to example filemanual/parameters2.pvl
Date2017-06-20

Statistical information

Lines of code18 lines (comments not included)
Lines of specification4 lines (22.22% of the total)
Computation time14523 milliseconds

Example code

Note, verification may take a while and has a time-out of 20 seconds.