wyc.lang

Class WhileyFile.Method

java.lang.Object

wybs.lang.SyntacticElement.Impl

wyc.lang.WhileyFile.NamedDeclaration

wyc.lang.WhileyFile.FunctionOrMethodOrProperty

wyc.lang.WhileyFile.Method

All Implemented Interfaces:

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

Enclosing class:

WhileyFile

public final class WhileyFile.Method
extends WhileyFile.FunctionOrMethodOrProperty

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

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

Here, a method m is defined which accepts only positive integers and returns only negative integers. The special variable $ is used to refer to the return value. Unlike functions, methods in Whiley may have side-effects.

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

NOTE see WhileyFile.FunctionOrMethodOrProperty for more information.

Author:

David J. Pearce

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.Method	resolvedType

Fields inherited from class wyc.lang.WhileyFile.FunctionOrMethodOrProperty

ensures, lifetimeParameters, parameters, requires, returns, statements

Constructor Summary

Constructors

Constructor and Description
Method(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)

Method Summary

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

Constructor Detail

Method

public Method(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)

Method Detail

unresolvedType

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

Specified by:

unresolvedType in class WhileyFile.FunctionOrMethodOrProperty

resolvedType

public Type.Method resolvedType()

Specified by:

resolvedType in class WhileyFile.FunctionOrMethodOrProperty