Libraries

A library is a file that contains either the specification of a data type or the specification of a set of functions, referred to as a unit.

These libraries, after being defined, can be imported into the applications specifications. This not only allows the user of the tool to reutilize code but also helps the user understand how different data types impact the coordination that is needed by the application more easily.

Examples of library files can be found in the specifications/library directory present in the Git Hub repository.

Data Types

• The specifications/library/set.spec file is an example of a data type specification which can be imported into application specifications.
• Only one data type can be specified per file.
• The specification must contain the following sections:
  • @type followed by the String datatype
  • @name followed by the identifier of the library file, which must be different in all library files.
  • @content followed by the data type specification in Boogie. Everything written here is copied to the top of the specification that imports this data type.
  • @equals followed by a Boogie expression that denotes equality between two instances of the data type being specified, in a similar fashion to what is required in application specifications. Here, @this and @other are used to denote the two different instances that are being compared.
• The order here presented for the sections must respected and none of them are optional.

Units

• The specifications/library/map1k_utils.spec is an example of a unit specification (it contains a default implementation for an "equals" function of a 1key-1value map, among other things).
• The specification must contain the following sections:
  • @type followed by the String unit
  • @name followed by the identifier of the library file, which must be different in all library files.
  • @content followed by the content of the unit, specified in Boogie. Everything written here is copied to the top of the specification that imports this unit.
• The order here presented for the sections must respected and none of them are optional.

Notes

• Currently, when copying the libraries to the top of the application specifications at run time, the tool does not verify if any of the identifiers in the resulting specifications collide. As such, when adding a new identifier to a library the name of the library should be used as a suffix.

Example

This is the specifications/library/set.spec file found in the repository.

@type datatype
@name Set


@content

type Set = <a>[a]bool;

function setAdd<a>(element:a, set: Set, oldSet: Set)returns(bool)
{
    (forall <b> e: b :: 
    ((e != element) ==> (set[e] == oldSet[e])) && 
    ((e == element) ==> (set[element] == true)))
}

function setRemove<a>(element:a, set: Set, oldSet: Set)returns(bool)
{
    (forall <b> e: b :: 
    ((e != element) ==> (set[e] == oldSet[e])) && 
    ((e == element) ==> (set[element] == false)))
}

function setIn<a>(element:a, set: Set)returns(bool)
{
    (set[element])
}

@equals forall <a> e: a :: @this[e] == @other[e];