wyc.lang

Class WhileyFile.FunctionOrMethodOrProperty

java.lang.Object

wybs.lang.SyntacticElement.Impl

wyc.lang.WhileyFile.NamedDeclaration

wyc.lang.WhileyFile.FunctionOrMethodOrProperty

All Implemented Interfaces:

wybs.lang.SyntacticElement, WhileyFile.Context, WhileyFile.Declaration

Direct Known Subclasses:

WhileyFile.Function, WhileyFile.Method, WhileyFile.Property

Enclosing class:

WhileyFile

public abstract class WhileyFile.FunctionOrMethodOrProperty
extends WhileyFile.NamedDeclaration

Represents a function declaration or method declaration in a Whiley source file which have the form:

 FunctionDeclaration ::= "function" TypePattern "=>" TypePattern (FunctionMethodClause)* ':' NewLine Block

 MethodDeclaration ::= "method" TypePattern "=>" TypePattern (FunctionMethodClause)* ':' NewLine Block

 FunctionMethodClause ::= "throws" Type | "requires" Expression | "ensures" Expression
 

Here, the first type pattern (i.e. before "=>") is referred to as the "parameter", whilst the second is referred to as the "return". There are three kinds of option clause:

• Throws clause. This defines the exceptions which may be thrown by this function. Multiple clauses may be given, and these are taken together as a union. Furthermore, the convention is to specify the throws clause before the others.
• Requires clause. This defines a constraint on the permissible values of the parameters on entry to the function or method, and is often referred to as the "precondition". This expression may refer to any variables declared within the parameter type pattern. Multiple clauses may be given, and these are taken together as a conjunction. Furthermore, the convention is to specify the requires clause(s) before any ensure(s) clauses.
• Ensures clause. This defines a constraint on the permissible values of the the function or method's return value, and is often referred to as the "postcondition". This expression may refer to any variables declared within either the parameter or return type pattern. Multiple clauses may be given, and these are taken together as a conjunction. Furthermore, the convention is to specify the requires clause(s) after the others.

The following function declaration provides a small example to illustrate:

 function max(int x, int y) -> (int z)
 // return must be greater than either parameter
 ensures x <= z && y <= z
 // return must equal one of the parmaeters
 ensures x == z || y == z:
     ...
 

Here, we see the specification for the well-known max() function which returns the largest of its parameters. This does not throw any exceptions, and does not enforce any preconditions on its parameters.

Function and method declarations may also have modifiers, such as public and private.

Nested Class Summary

Nested classes/interfaces inherited from interface wybs.lang.SyntacticElement

wybs.lang.SyntacticElement.Impl

Field Summary

Fields

Modifier and Type	Field and Description
List<Expr>	ensures
ArrayList<String>	lifetimeParameters
ArrayList<WhileyFile.Parameter>	parameters
List<Expr>	requires
ArrayList<WhileyFile.Parameter>	returns
ArrayList<Stmt>	statements

Constructor Summary

Constructors

Constructor and Description
FunctionOrMethodOrProperty(List<Modifier> modifiers, String name, List<WhileyFile.Parameter> returns, List<WhileyFile.Parameter> parameters, List<String> lifetimeParameters, List<Expr> requires, List<Expr> ensures, List<Stmt> statements, wybs.lang.Attribute... attributes) Construct an object representing a Whiley function.

Method Summary

Modifier and Type	Method and Description
abstract Type.FunctionOrMethod	resolvedType()
abstract wyal.lang.WyalFile.Type.FunctionOrMethodOrProperty	unresolvedType()

Methods inherited from class wyc.lang.WhileyFile.NamedDeclaration

hasModifier, modifiers, name

Methods inherited from class wybs.lang.SyntacticElement.Impl

attribute, attributes

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface wybs.lang.SyntacticElement

attribute, attributes

Field Detail

parameters

public final ArrayList<WhileyFile.Parameter> parameters

lifetimeParameters

public final ArrayList<String> lifetimeParameters

returns

public final ArrayList<WhileyFile.Parameter> returns

statements

public final ArrayList<Stmt> statements

requires

public List<Expr> requires

ensures

public List<Expr> ensures

Constructor Detail

FunctionOrMethodOrProperty

public FunctionOrMethodOrProperty(List<Modifier> modifiers,
                                  String name,
                                  List<WhileyFile.Parameter> returns,
                                  List<WhileyFile.Parameter> parameters,
                                  List<String> lifetimeParameters,
                                  List<Expr> requires,
                                  List<Expr> ensures,
                                  List<Stmt> statements,
                                  wybs.lang.Attribute... attributes)

Construct an object representing a Whiley function.

Parameters:

name - - The name of the function.

returnType - - The return type of this method

paramTypes - - The list of parameter names and their types for this method

requires - - The constraints which must hold true on entry

ensures - - The constraints which must hold true on exit

statements - - The Statements making up the function body.

Method Detail

unresolvedType

public abstract wyal.lang.WyalFile.Type.FunctionOrMethodOrProperty unresolvedType()

resolvedType

public abstract Type.FunctionOrMethod resolvedType()