Overview

Rosetta's function definition and evaluation capability provides function definition and application capabilities and a collection of advanced capabilities for more sophisticated and powerful specifications. Like functions in traditional functional programming languages, Rosetta functions provide a mechanism for defining abstractions of expressions over parameters. Unlike functions in traditional imperative programming languages, Rosetta functions are pure and side-effect free.

A Rosetta function simply reduces to a value derived from its parameters and items defined in its static scope. Actual parameters that Rosetta functions are applied to cannot be altered by the function application, nor can other symbols in the static scope be altered. Each Rosetta function is simply an encapsulated expression defined over its parameters and items in scope. When evaluated, the encapsulated expression simply reduces to a value that replaces the function application. In this sense, Rosetta functions behave more like mathematical functions than functions and procedures from programming languages.

Throughout this chapter, a simple increment function defined over an integer type is used to demonstrate function properties. Its declaration:

inc(x::integer)::integer <b class="bold">is</b> x+1;

defines a parameter and its type, and range type, and a defining expression. For any expression, a, when inc(a) appears in a specification, it can be reduced to a+1.

Direct definition using this style is the simplest and most common mechanism for defining functions, but it is not the only mechanism. Like other Rosetta items, functions have labels, types, and values. While the direct definition mechanism defines all three in one syntactic construct,...