wyc.lang

Class Stmt.DoWhile

java.lang.Object

wybs.lang.SyntacticElement.Impl

wyc.lang.Stmt.DoWhile

All Implemented Interfaces:

wybs.lang.SyntacticElement, Stmt

Enclosing interface:

Stmt

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

Represents a do-while statement whose body is made up from a block of statements separated by indentation. As an example:

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

Here, the where is optional, and commonly referred to as the loop invariant.

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
ArrayList<Expr>	invariants

Constructor Summary

Constructors

Constructor and Description
DoWhile(Expr condition, List<Expr> invariants, Collection<Stmt> body, wybs.lang.Attribute... attributes) Construct a Do-While statement from a given condition and body of statements.
DoWhile(Expr condition, List<Expr> invariants, Collection<Stmt> body, Collection<wybs.lang.Attribute> attributes) Construct a Do-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 final ArrayList<Expr> invariants

body

public final ArrayList<Stmt> body

Constructor Detail

DoWhile

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

Construct a Do-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 -

DoWhile

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

Construct a Do-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 -