Signature File

Danish uses a signature file to specify the signatures, or return types and parameter lists, of each method used in axiom specifications.

To clarify an important difference: Specifying a method without a parameter list generates code without parenthesis following the method name, where as specifying a method with an empty parameter list generates code with parenthesis but no parameters. Danish uses functional notation, which may be confusing with the use of an object oriented program such as Java. The point of confusion comes with a member function, which in functional notation returns an object type and takes an object type as a parameter. To illustrate, a member function 'class.function(value)' is actually 'class = function(class, value)'.

Notation/Syntax

The following is the notation for each line of a signature in the signature file: 

	"return type" "function name"
			OR
	"return type" "function name" ("type list")

Curly braces are used to indicate the location of the class parameter; they are placed around the parameter which represents the instance of which the function is a member. If a member is a mutator class, the return type is in effect the class itself; this is indicated by enclosing the return type in braces.

Examples

(SEE: Alias file for details of single word functions) 
	{class}  function ({class}, Id, value)
	>would be the form for a mutator function of the class
		 (changes the class/object itself, ex: add)

	Id newId (int)
	>would be the form to return an Id type with an int as
		 a parameter

	class newClass ()
	>would be the form to create a new instance of a class

	attr nullAttr
	>would be the form for a function with no parameters

	{class} function (int)
	>is invalid, since this must have the class as a parameter

Danish performs strong type checking; it supports overloaded function names so a single function name may have multiple signatures as long as they are distinguishable. The wildcard '*' is a valid parameter type name and will accept any variable of any type.

Printing Functions

A signature which has a return type of an empty pair of braces (i.e. nothing is returned and it is returned by side effect) signifies a function which will print a variable of the type of its one parameter. The type may be enclosed in braces if the printing function is a method of the type.

When an axiom fails, the printing function (if it exists) is invoked for the failing lvalue and rvalue.

Known Types and Functions

Danish knows the types 'int', 'boolean', 'String' and 'char'.

Integers are specified by an optional negative sign followed by one or more digits; type 'boolean' can be either 'true' or 'false; Strings are enclosed in double quotes, chars in single quotes. 

	RETURN_TYPE	OPERATOR	OPERANDS	NOTES
	   boolean	   ==		 (*,*)		-equal
	   boolean	   &&		(bool, bool)	-and
	   boolean	   ^^		(bool, bool)
	   boolean	   !=		 (*,*)		-not equal
	   boolean	   ||		(bool, bool)	-or

	   int		   +		(int, int)	-addition
	   int		   -		(int, int)	-subtraction
	   int		   *		(int, int)	-multiply
	   int		   /		(int, int)	-division
	   int		   %		(int, int)	-modulus

	NOTE:  operand * signifies any type.

Built in infix functions are listed above. Evaluation of all expressions in strictly right to left; there is no precedence. 'a == b ? c : d' will be interpreted as 'a == (b ? c : d)'. The use of parentheses is highly recommended. The only other built in function is 'boolean not (boolean)'.

Conditional evaluation is performed with the ternary operator: 

	"if boolean" ? "then clause" : "else clause".

>adapted from Daistish++ manual, by Hughes, September 25, 1995.

Goto Previous Topic Goto Next Topic
Created 02/11/98 by kennedy
Modified 04/27/98