wyc.lang

Class WhileyFile.Function

java.lang.Object

wybs.lang.SyntacticElement.Impl

wyc.lang.WhileyFile.NamedDeclaration

wyc.lang.WhileyFile.FunctionOrMethodOrProperty

wyc.lang.WhileyFile.Function

All Implemented Interfaces:

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

Enclosing class:

WhileyFile

public final class WhileyFile.Function
extends WhileyFile.FunctionOrMethodOrProperty

Represents a function declaration in a Whiley source file. For example:

 function f(int x) -> (int y)
 // Parameter must be positive
 requires x > 0
 // Return must be negative
 ensures y < 0:
    // body
    return -x
 

Here, a function f is defined which accepts only positive integers and returns only negative integers. The special variable $ is used to refer to the return value. Functions in Whiley may not have side-effects (i.e. they are pure functions).

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

NOTE see WhileyFile.FunctionOrMethodOrProperty for more information.

Author:

David J. Pearce

See Also:

WhileyFile.FunctionOrMethodOrProperty

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
Type.Function	resolvedType

Fields inherited from class wyc.lang.WhileyFile.FunctionOrMethodOrProperty

ensures, lifetimeParameters, parameters, requires, returns, statements

Constructor Summary

Constructors

Constructor and Description
Function(List<Modifier> modifiers, String name, List<WhileyFile.Parameter> returns, List<WhileyFile.Parameter> parameters, List<Expr> requires, List<Expr> ensures, List<Stmt> statements, wybs.lang.Attribute... attributes)

Method Summary

Modifier and Type	Method and Description
Type.Function	resolvedType()
wyal.lang.WyalFile.Type.Function	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

resolvedType

public Type.Function resolvedType

Constructor Detail

Function

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

Method Detail

unresolvedType

public wyal.lang.WyalFile.Type.Function unresolvedType()

Specified by:

unresolvedType in class WhileyFile.FunctionOrMethodOrProperty

resolvedType

public Type.Function resolvedType()

Specified by:

resolvedType in class WhileyFile.FunctionOrMethodOrProperty