Class DoWhile

src/main/java/wyil/lang/WyilFile.java:2062–2107

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 <p

		 *
		 */
		public static class DoWhile extends AbstractItem implements Loop {
			public DoWhile(Expr condition, Tuple<Expr> invariant, Tuple<Decl.Variable> modified, Stmt.Block body) {
				super(STMT_dowhile, condition, invariant, modified, body);
			}

			public Expr getCondition() {
				return (Expr) super.get(0);
			}

			@Override
			@SuppressWarnings("unchecked")
			public Tuple<Expr> getInvariant() {
				return (Tuple<Expr>) super.get(1);
			}

			@Override
			@SuppressWarnings("unchecked")
			public Tuple<Decl.Variable> getModified() {
				return (Tuple<Decl.Variable>) super.get(2);
			}

			public void setModified(Tuple<Decl.Variable> modified) {
				operands[2] = modified;
			}

			@Override
			public Stmt.Block getBody() {
				return (Stmt.Block) super.get(3);
			}

			@SuppressWarnings("unchecked")
			@Override
			public Syntactic.Item clone(Syntactic.Item[] operands) {
				return new DoWhile((Expr) operands[0], (Tuple<Expr>) operands[1], (Tuple<Decl.Variable>) operands[2],
						(Stmt.Block) operands[3]);
			}

			public static final Descriptor DESCRIPTOR_0 = new Descriptor(Operands.FOUR, Data.ZERO, "STMT_dowhile") {
				@SuppressWarnings("unchecked")
				@Override
				public Syntactic.Item construct(int opcode, Syntactic.Item[] operands, byte[] data) {
					return new DoWhile((Expr) operands[0], (Tuple<Expr>) operands[1],
							(Tuple<Decl.Variable>) operands[2], (Stmt.Block) operands[3]);
				}
			};
		}

		/**
		 * Represents a fail statement for the form "<code>fail</code>". This causes an