function

A function in Cyclone is a building block that can be used for constructing complex computation, it is just like functions in other programming languages.

Syntax

The syntax for defining a function is as follows:

function name:return_type ([var_name:type]*){

    (expression)* return expression;

 }

The name here is a function name and return_type is its return type. The var_name:type defines a list of arguments and their types and it is optional. Everything enclosed between { and } is a function body.

Scope

A function is declared before defining nodes. In other words, a function is defined where a variable is defined in a specification.

Semantics

The semantic rules for a function in Cyclone are as follows:

• a function must have its unique name
• a function must return a value
• a function cannot be used inside a where clause
• a function is non-recursive
• a function can be used over int, bool and real

Examples

 function add:int(x:int ,y:int) { 

      return  x+y; 

 }

 option-trace=true;

 machine Intersect {

 int x; 

 function f:int(x:int) { 

      return  2*x+1; 

 }

 function g:int(x:int) { 

      return  x*x*x; 

 }

 function h:int(x:int) { 

      return  1/x; 

 }

 normal start final state S{}

 trans { S -> S }

  goal{

      assert some(f(x)==g(x) && g(x)==h(x));

      check for 1

    }

}

@2020-2023 Hao Wu. All rights reserved. Last update: 06 July, 2023