wyc.lang

Class Stmt.While

java.lang.Object

wybs.lang.SyntacticElement.Impl

wyc.lang.Stmt.While

All Implemented Interfaces:

wybs.lang.SyntacticElement, Stmt

Enclosing interface:

Stmt

public static final class Stmt.While
extends wybs.lang.SyntacticElement.Impl
implements Stmt

Represents a while statement, which has the form:

 WhileStmt ::= "while" Expression (where Expression)* ':' NewLine Block
 

As an example:

 function sum([int] xs) -> int:
   int r = 0
   int i = 0
   while i < |xs| where i >= 0:
     r = r + xs[i]
     i = i + 1
   return r
 

The optional where clause(s) are commonly referred to as the "loop invariant". When multiple clauses are given, these are combined using a conjunction. The combined invariant defines a condition which must be true on every iteration of the loop.

Author:

David J. Pearce

Nested Class Summary

Nested classes/interfaces inherited from interface wyc.lang.Stmt

Stmt.Assert, Stmt.Assign, Stmt.Assume, Stmt.Break, Stmt.Case, Stmt.Continue, Stmt.Debug, Stmt.DoWhile, Stmt.Fail, Stmt.IfElse, Stmt.NamedBlock, Stmt.Return, Stmt.Skip, Stmt.Switch, Stmt.VariableDeclaration, Stmt.While

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

wybs.lang.SyntacticElement.Impl

Field Summary

Fields

Modifier and Type	Field and Description
ArrayList<Stmt>	body
Expr	condition
List<Expr>	invariants

Constructor Summary

Constructors

Constructor and Description
While(Expr condition, List<Expr> invariants, Collection<Stmt> body, wybs.lang.Attribute... attributes) Construct a While statement from a given condition and body of statements.
While(Expr condition, List<Expr> invariants, Collection<Stmt> body, Collection<wybs.lang.Attribute> attributes) Construct a While statement from a given condition and body of statements.

Method Summary

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

condition

public Expr condition

invariants

public List<Expr> invariants

body

public final ArrayList<Stmt> body

Constructor Detail

While

public While(Expr condition,
             List<Expr> invariants,
             Collection<Stmt> body,
             wybs.lang.Attribute... attributes)

Construct a While statement from a given condition and body of statements.

Parameters:

condition - non-null expression.

invariant - The loop invariant expression, which may be null (if no invariant is given)

body - non-null collection which contains zero or more statements.

attributes -

While

public While(Expr condition,
             List<Expr> invariants,
             Collection<Stmt> body,
             Collection<wybs.lang.Attribute> attributes)

Construct a While statement from a given condition and body of statements.

Parameters:

condition - non-null expression.

invariant - The loop invariant expression, which may be null (if no invariant is given)

body - non-null collection which contains zero or more statements.

attributes -