CVL functions allow you to reuse parts of a specification, such as common assumptions, assertions, or basic calculations. Additionally they can be used for basic calculations and for function summaries.


The syntax for CVL functions is given by the following EBNF grammar:

function ::= [ "override" ]
             "function" id
             [ "(" params ")" ]
             [ "returns" type ]

See Basic Syntax for the id production, Types for the type production, and Statements for the block production.


Using CVL functions

CVL Function may be called from within a rule, or from within another CVL function.