public static final class AuxiliaryContractBuilders.ValidityProgramConstructor
extends java.lang.Object
block'
from block
(see Wacker 2012, 3.3).construct()
Constructor and Description |
---|
ValidityProgramConstructor(java.lang.Iterable<Label> labels,
StatementBlock block,
AuxiliaryContract.Variables variables,
ProgramVariable exceptionParameter,
Services services) |
ValidityProgramConstructor(java.lang.Iterable<Label> labels,
StatementBlock block,
AuxiliaryContract.Variables variables,
ProgramVariable exceptionParameter,
Services services,
AuxiliaryContract.Variables alreadyDeclared) |
Modifier and Type | Method and Description |
---|---|
StatementBlock |
construct() |
public ValidityProgramConstructor(java.lang.Iterable<Label> labels, StatementBlock block, AuxiliaryContract.Variables variables, ProgramVariable exceptionParameter, Services services)
labels
- all labels belonging to the block.block
- the block.variables
- the variables.exceptionParameter
- the exception variable.services
- services.public ValidityProgramConstructor(java.lang.Iterable<Label> labels, StatementBlock block, AuxiliaryContract.Variables variables, ProgramVariable exceptionParameter, Services services, AuxiliaryContract.Variables alreadyDeclared)
labels
- all labels belonging to the block.block
- the block.variables
- the variables.exceptionParameter
- the exception variable.services
- services.alreadyDeclared
- the subset of variables that have already been declared.public StatementBlock construct()
Copyright © 2003-2019 The KeY-Project.