JMLSpecFactory (KeY API Documentation)

java.lang.Object
- de.uka.ilkd.key.speclang.jml.translation.JMLSpecFactory

```
public class JMLSpecFactory
extends java.lang.Object
```
A factory for creating class invariants and operation contracts from textual JML specifications. This is the public interface to the jml.translation package.

Nested Class Summary

Nested Classes
Modifier and Type Class and Description

private static class JMLSpecFactory.ContractClauses

Nested Classes
Modifier and Type	Class and Description
`private static class`	`JMLSpecFactory.ContractClauses`

Field Summary

Fields
Modifier and Type	Field and Description
`private ContractFactory`	`cf`
`private int`	`invCounter`
`private java.util.Set<Pair<KeYJavaType,IObserverFunction>>`	`modelFields` Used to check that there is only one represents clause per type and field.
`private Services`	`services`
`private TermBuilder`	`tb`

Constructor Summary

Constructors
Constructor and Description

JMLSpecFactory(Services services)

Constructors
Constructor and Description
`JMLSpecFactory(Services services)`

Method Summary

All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type	Method and Description
`private ImmutableList<ProgramVariable>`	`append(ImmutableList<ProgramVariable> localVars, ImmutableList<LocationVariable> paramVars)`
`private ImmutableList<ProgramVariable>`	`collectLocalVariables(StatementContainer sc, LoopStatement loop)` Collects local variables of the passed statement that are visible for the passed loop.
`protected ImmutableList<ProgramVariable>`	`collectLocalVariablesVisibleTo(Statement statement, IProgramMethod method)`
`private ImmutableList<ProgramVariable>`	`collectLocalVariablesVisibleTo(Statement statement, StatementContainer container)`
`private static java.util.Map<LocationVariable,Term>`	`createAtPres(ImmutableList<LocationVariable> paramVars, ImmutableList<LocationVariable> allHeaps, TermBuilder tb)`
`private ImmutableSet<Contract>`	`createDependencyOperationContract(IProgramMethod pm, ProgramVariableCollection progVars, JMLSpecFactory.ContractClauses clauses)` Generate dependency operation contract out of the JML accessible clause.
`private ImmutableSet<Contract>`	`createFunctionalOperationContracts(java.lang.String name, IProgramMethod pm, ProgramVariableCollection progVars, JMLSpecFactory.ContractClauses clauses, java.util.Map<LocationVariable,Term> posts, java.util.Map<LocationVariable,Term> axioms)` Generate functional operation contracts.
`private ImmutableSet<Contract>`	`createInformationFlowContracts(JMLSpecFactory.ContractClauses clauses, IProgramMethod pm, ProgramVariableCollection progVars)`
`ImmutableSet<BlockContract>`	`createJMLBlockContracts(IProgramMethod method, java.util.List<Label> labels, StatementBlock block, TextualJMLSpecCase specificationCase)` Creates a set of block contracts for a block from a textual specification case.
`ClassAxiom`	`createJMLClassAxiom(KeYJavaType kjt, TextualJMLClassAxiom textual)` Creates a class axiom from a textual JML representation.
`ClassInvariant`	`createJMLClassInvariant(KeYJavaType kjt, TextualJMLClassInv textualInv)`
`ClassInvariant`	`createJMLClassInvariant(KeYJavaType kjt, VisibilityModifier visibility, boolean isStatic, PositionedString originalInv)`
`Contract`	`createJMLDependencyContract(KeYJavaType kjt, LocationVariable targetHeap, PositionedString originalDep)`
`Contract`	`createJMLDependencyContract(KeYJavaType kjt, TextualJMLDepends textualDep)`
`InitiallyClause`	`createJMLInitiallyClause(KeYJavaType kjt, TextualJMLInitially textualInv)`
`InitiallyClause`	`createJMLInitiallyClause(KeYJavaType kjt, VisibilityModifier visibility, PositionedString original)`
`ImmutableSet<LoopContract>`	`createJMLLoopContracts(IProgramMethod method, java.util.List<Label> labels, LoopStatement loop, TextualJMLSpecCase specificationCase)` Creates a set of loop contracts for a loop from a textual specification case.
`ImmutableSet<LoopContract>`	`createJMLLoopContracts(IProgramMethod method, java.util.List<Label> labels, StatementBlock block, TextualJMLSpecCase specificationCase)` Creates a set of loop contracts for a block from a textual specification case.
`private LoopSpecification`	`createJMLLoopInvariant(IProgramMethod pm, LoopStatement loop, java.util.Map<java.lang.String,ImmutableList<PositionedString>> originalInvariants, java.util.Map<java.lang.String,ImmutableList<PositionedString>> originalFreeInvariants, java.util.Map<java.lang.String,ImmutableList<PositionedString>> originalAssignables, ImmutableList<PositionedString> originalInfFlowSpecs, PositionedString originalVariant)`
`LoopSpecification`	`createJMLLoopInvariant(IProgramMethod pm, LoopStatement loop, TextualJMLLoopSpec textualLoopSpec)`
`ImmutableSet<MergeContract>`	`createJMLMergeContracts(IProgramMethod method, MergePointStatement mps, TextualJMLMergePointDecl mergePointDecl, ImmutableList<ProgramVariable> methodParams)`
`ImmutableSet<Contract>`	`createJMLOperationContracts(IProgramMethod pm, TextualJMLSpecCase textualSpecCase)` Creates operation contracts out of the passed JML specification.
`ClassAxiom`	`createJMLRepresents(KeYJavaType kjt, TextualJMLRepresents textualRep)`
`ClassAxiom`	`createJMLRepresents(KeYJavaType kjt, VisibilityModifier visibility, PositionedString originalRep, boolean isStatic)`
`private ImmutableList<PositionedString>`	`createPrecond(IProgramMethod pm, PositionedString originalSpec)`
`private ProgramVariableCollection`	`createProgramVariables(IProgramMethod pm)`
`private ProgramVariableCollection`	`createProgramVariables(IProgramMethod method, JavaStatement block, AuxiliaryContract.Variables variables)` Creates a program variable collection for a specified block.
`private java.lang.String`	`generateName(IProgramMethod pm, TextualJMLSpecCase textualSpecCase, Behavior originalBehavior)`
`private java.util.Map<LocationVariable,Term>`	`generatePostCondition(ProgramVariableCollection progVars, JMLSpecFactory.ContractClauses clauses, Behavior originalBehavior)`
`private java.util.Map<LocationVariable,Term>`	`generateRepresentsAxioms(ProgramVariableCollection progVars, JMLSpecFactory.ContractClauses clauses, Behavior originalBehavior)`
`private java.lang.String`	`getContractName(IProgramMethod programMethod, Behavior behavior)`
`private java.lang.String`	`getDefaultInvName(java.lang.String name, KeYJavaType kjt)`
`private java.lang.String`	`getInicName()`
`private VisibilityModifier`	`getVisibility(TextualJMLConstruct textualConstruct)`
`FunctionalOperationContract`	`initiallyClauseToContract(InitiallyClause ini, IProgramMethod pm)` Translate initially clause to a contract for the given constructor.
`private ImmutableList<Term>`	`registerAbbreviationVariables(TextualJMLSpecCase textualSpecCase, KeYJavaType inClass, ProgramVariableCollection progVars, JMLSpecFactory.ContractClauses clauses)` register abbreviations in contracts (aka. old clauses). creates update terms.
`private java.util.Map<LocationVariable,Term>`	`termify(java.util.Map<LocationVariable,LocationVariable> remembranceVariables)`
`private void`	`translateAccessible(IProgramMethod pm, ProgramVariableCollection progVars, LocationVariable heap, ProgramVariable heapAtPre, LocationVariable savedHeap, ImmutableList<PositionedString> accessible, ImmutableList<PositionedString> accessiblePre, JMLSpecFactory.ContractClauses clauses)`
`private Term`	`translateAccessible(IProgramMethod pm, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,Term> atPres, java.util.Map<LocationVariable,Term> atBefores, ImmutableList<PositionedString> originalClauses)`
`private Term`	`translateAndClauses(IProgramMethod pm, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, java.util.Map<LocationVariable,Term> atPres, java.util.Map<LocationVariable,Term> atBefores, ImmutableList<PositionedString> originalClauses)` Clauses are expected to be conjoined in a right-associative way, i.e.
`private void`	`translateAssignable(IProgramMethod pm, ProgramVariableCollection progVars, LocationVariable heap, LocationVariable savedHeap, ImmutableList<PositionedString> mod, JMLSpecFactory.ContractClauses clauses)`
`private Term`	`translateAssignable(IProgramMethod pm, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,Term> atPres, java.util.Map<LocationVariable,Term> atBefores, ImmutableList<PositionedString> originalClauses)`
`private void`	`translateAxioms(IProgramMethod pm, ProgramVariableCollection progVars, LocationVariable heap, ImmutableList<PositionedString> axioms, JMLSpecFactory.ContractClauses clauses, Behavior originalBehavior)`
`private java.util.Map<Label,Term>`	`translateBreaks(IProgramMethod pm, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, java.util.Map<LocationVariable,Term> atPres, java.util.Map<LocationVariable,Term> atBefores, Behavior originalBehavior, ImmutableList<PositionedString> originalClauses)`
`private java.util.Map<Label,Term>`	`translateContinues(IProgramMethod pm, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, java.util.Map<LocationVariable,Term> atPres, java.util.Map<LocationVariable,Term> atBefores, Behavior originalBehavior, ImmutableList<PositionedString> originalClauses)`
`private Term`	`translateDecreases(IProgramMethod pm, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,Term> atPres, java.util.Map<LocationVariable,Term> atBefores, ImmutableList<PositionedString> originalDecreases)`
`private void`	`translateEnsures(IProgramMethod pm, ProgramVariableCollection progVars, LocationVariable heap, LocationVariable savedHeap, ImmutableList<PositionedString> ensures, ImmutableList<PositionedString> ensuresFree, JMLSpecFactory.ContractClauses clauses, Behavior originalBehavior)`
`private Term`	`translateEnsures(IProgramMethod pm, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, java.util.Map<LocationVariable,Term> atPres, java.util.Map<LocationVariable,Term> atBefores, Behavior originalBehavior, ImmutableList<PositionedString> originalClauses)`
`private ImmutableList<InfFlowSpec>`	`translateInfFlowSpecClauses(IProgramMethod pm, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, ImmutableList<PositionedString> originalClauses)`
`private JMLSpecFactory.ContractClauses`	`translateJMLClauses(IProgramMethod pm, TextualJMLSpecCase textualSpecCase, ProgramVariableCollection progVars, Behavior originalBehavior)`
`private Term`	`translateMeasuredBy(IProgramMethod pm, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ImmutableList<PositionedString> originalMeasuredBy)`
`private Term`	`translateOrClauses(IProgramMethod pm, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ImmutableList<PositionedString> originalClauses)`
`private void`	`translateRequires(IProgramMethod pm, ProgramVariableCollection progVars, LocationVariable heap, LocationVariable savedHeap, ImmutableList<PositionedString> requires, ImmutableList<PositionedString> requiresFree, JMLSpecFactory.ContractClauses clauses)`
`private Term`	`translateReturns(IProgramMethod pm, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, java.util.Map<LocationVariable,Term> atPres, java.util.Map<LocationVariable,Term> atBefores, Behavior originalBehavior, ImmutableList<PositionedString> originalClauses)`
`private Term`	`translateSignals(IProgramMethod pm, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, java.util.Map<LocationVariable,Term> atPres, java.util.Map<LocationVariable,Term> atBefores, Behavior originalBehavior, ImmutableList<PositionedString> originalClauses)`
`private Term`	`translateSignalsOnly(IProgramMethod pm, ProgramVariable excVar, Behavior originalBehavior, ImmutableList<PositionedString> originalClauses)`
`private boolean`	`translateStrictlyPure(IProgramMethod pm, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ImmutableList<PositionedString> assignableClauses)`
`private java.util.Map<LocationVariable,Term>`	`translateToTermAsssignable(IProgramMethod pm, ProgramVariable selfVar, java.util.Map<LocationVariable,Term> atPres, ImmutableList<ProgramVariable> allVars, java.util.Map<java.lang.String,ImmutableList<PositionedString>> originalAssignables)`
`private static java.util.Map<LocationVariable,Term>`	`translateToTermFreeInvariants(IProgramMethod pm, java.util.Map<java.lang.String,ImmutableList<PositionedString>> originalFreeInvariants, ProgramVariable selfVar, ImmutableList<ProgramVariable> allVars, ImmutableList<LocationVariable> allHeaps, java.util.Map<LocationVariable,Term> atPres, Services services, TermBuilder tb)`
`private java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>>`	`translateToTermInfFlowSpecs(IProgramMethod pm, ProgramVariable selfVar, ProgramVariable resultVar, ProgramVariable excVar, ImmutableList<ProgramVariable> allVars, ImmutableList<LocationVariable> allHeaps, ImmutableList<PositionedString> originalInfFlowSpecs)`
`private static java.util.Map<LocationVariable,Term>`	`translateToTermInvariants(IProgramMethod pm, java.util.Map<java.lang.String,ImmutableList<PositionedString>> originalInvariants, ProgramVariable selfVar, ImmutableList<ProgramVariable> allVars, ImmutableList<LocationVariable> allHeaps, java.util.Map<LocationVariable,Term> atPres, Services services, TermBuilder tb)`
`private Term`	`translateToTermVariant(IProgramMethod pm, ProgramVariable selfVar, java.util.Map<LocationVariable,Term> atPres, ImmutableList<ProgramVariable> allVars, PositionedString originalVariant)`
`private Term`	`translateUnionClauses(IProgramMethod pm, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, java.util.Map<LocationVariable,Term> atPres, java.util.Map<LocationVariable,Term> atBefores, ImmutableList<PositionedString> originalClauses)`

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

tb
```
private final TermBuilder tb
```

services
```
private final Services services
```

cf
```
private final ContractFactory cf
```

invCounter
```
private int invCounter
```

modelFields
```
private java.util.Set<Pair<KeYJavaType,IObserverFunction>> modelFields
```
Used to check that there is only one represents clause per type and field.

Constructor Detail

JMLSpecFactory

public JMLSpecFactory(Services services)

Method Detail

createAtPres

private static java.util.Map<LocationVariable,Term> createAtPres(ImmutableList<LocationVariable> paramVars,
                                                                 ImmutableList<LocationVariable> allHeaps,
                                                                 TermBuilder tb)

translateToTermInvariants

private static java.util.Map<LocationVariable,Term> translateToTermInvariants(IProgramMethod pm,
                                                                              java.util.Map<java.lang.String,ImmutableList<PositionedString>> originalInvariants,
                                                                              ProgramVariable selfVar,
                                                                              ImmutableList<ProgramVariable> allVars,
                                                                              ImmutableList<LocationVariable> allHeaps,
                                                                              java.util.Map<LocationVariable,Term> atPres,
                                                                              Services services,
                                                                              TermBuilder tb)
                                                                       throws SLTranslationException

Throws:: SLTranslationException

translateToTermFreeInvariants

private static java.util.Map<LocationVariable,Term> translateToTermFreeInvariants(IProgramMethod pm,
                                                                                  java.util.Map<java.lang.String,ImmutableList<PositionedString>> originalFreeInvariants,
                                                                                  ProgramVariable selfVar,
                                                                                  ImmutableList<ProgramVariable> allVars,
                                                                                  ImmutableList<LocationVariable> allHeaps,
                                                                                  java.util.Map<LocationVariable,Term> atPres,
                                                                                  Services services,
                                                                                  TermBuilder tb)
                                                                           throws SLTranslationException

Throws:: SLTranslationException

createInformationFlowContracts

private ImmutableSet<Contract> createInformationFlowContracts(JMLSpecFactory.ContractClauses clauses,
                                                              IProgramMethod pm,
                                                              ProgramVariableCollection progVars)

getDefaultInvName

private java.lang.String getDefaultInvName(java.lang.String name,
                                           KeYJavaType kjt)

getInicName

private java.lang.String getInicName()

getContractName

private java.lang.String getContractName(IProgramMethod programMethod,
                                         Behavior behavior)

collectLocalVariables

private ImmutableList<ProgramVariable> collectLocalVariables(StatementContainer sc,
                                                             LoopStatement loop)

Collects local variables of the passed statement that are visible for the passed loop. Returns null if the loop has not been found.

getVisibility

private VisibilityModifier getVisibility(TextualJMLConstruct textualConstruct)

createProgramVariables

private ProgramVariableCollection createProgramVariables(IProgramMethod pm)

translateJMLClauses

private JMLSpecFactory.ContractClauses translateJMLClauses(IProgramMethod pm,
                                                           TextualJMLSpecCase textualSpecCase,
                                                           ProgramVariableCollection progVars,
                                                           Behavior originalBehavior)
                                                    throws SLTranslationException

Throws:: SLTranslationException

translateAccessible

private void translateAccessible(IProgramMethod pm,
                                 ProgramVariableCollection progVars,
                                 LocationVariable heap,
                                 ProgramVariable heapAtPre,
                                 LocationVariable savedHeap,
                                 ImmutableList<PositionedString> accessible,
                                 ImmutableList<PositionedString> accessiblePre,
                                 JMLSpecFactory.ContractClauses clauses)
                          throws SLTranslationException

Throws:: SLTranslationException

translateAxioms

private void translateAxioms(IProgramMethod pm,
                             ProgramVariableCollection progVars,
                             LocationVariable heap,
                             ImmutableList<PositionedString> axioms,
                             JMLSpecFactory.ContractClauses clauses,
                             Behavior originalBehavior)
                      throws SLTranslationException

Throws:: SLTranslationException

translateEnsures

private void translateEnsures(IProgramMethod pm,
                              ProgramVariableCollection progVars,
                              LocationVariable heap,
                              LocationVariable savedHeap,
                              ImmutableList<PositionedString> ensures,
                              ImmutableList<PositionedString> ensuresFree,
                              JMLSpecFactory.ContractClauses clauses,
                              Behavior originalBehavior)
                       throws SLTranslationException

Throws:: SLTranslationException

translateRequires

private void translateRequires(IProgramMethod pm,
                               ProgramVariableCollection progVars,
                               LocationVariable heap,
                               LocationVariable savedHeap,
                               ImmutableList<PositionedString> requires,
                               ImmutableList<PositionedString> requiresFree,
                               JMLSpecFactory.ContractClauses clauses)
                        throws SLTranslationException

Throws:: SLTranslationException

translateAssignable

private void translateAssignable(IProgramMethod pm,
                                 ProgramVariableCollection progVars,
                                 LocationVariable heap,
                                 LocationVariable savedHeap,
                                 ImmutableList<PositionedString> mod,
                                 JMLSpecFactory.ContractClauses clauses)
                          throws SLTranslationException

Throws:: SLTranslationException

registerAbbreviationVariables

private ImmutableList<Term> registerAbbreviationVariables(TextualJMLSpecCase textualSpecCase,
                                                          KeYJavaType inClass,
                                                          ProgramVariableCollection progVars,
                                                          JMLSpecFactory.ContractClauses clauses)
                                                   throws SLTranslationException

Throws:: SLTranslationException

translateInfFlowSpecClauses

private ImmutableList<InfFlowSpec> translateInfFlowSpecClauses(IProgramMethod pm,
                                                               ProgramVariable selfVar,
                                                               ImmutableList<ProgramVariable> paramVars,
                                                               ProgramVariable resultVar,
                                                               ProgramVariable excVar,
                                                               ImmutableList<PositionedString> originalClauses)
                                                        throws SLTranslationException

Throws:: SLTranslationException

translateAndClauses

private Term translateAndClauses(IProgramMethod pm,
                                 ProgramVariable selfVar,
                                 ImmutableList<ProgramVariable> paramVars,
                                 ProgramVariable resultVar,
                                 ProgramVariable excVar,
                                 java.util.Map<LocationVariable,Term> atPres,
                                 java.util.Map<LocationVariable,Term> atBefores,
                                 ImmutableList<PositionedString> originalClauses)
                          throws SLTranslationException

Clauses are expected to be conjoined in a right-associative way, i.e. A & (B & ( C (...& N))). When using auto induction with lemmas, then A will be used as a lemma for B, A & B will be used as a lemma for C and so on. This mimics the Isabelle-style of proving.

Throws:: SLTranslationException

translateOrClauses

private Term translateOrClauses(IProgramMethod pm,
                                ProgramVariable selfVar,
                                ImmutableList<ProgramVariable> paramVars,
                                ImmutableList<PositionedString> originalClauses)
                         throws SLTranslationException

Throws:: SLTranslationException

translateUnionClauses

private Term translateUnionClauses(IProgramMethod pm,
                                   ProgramVariable selfVar,
                                   ImmutableList<ProgramVariable> paramVars,
                                   java.util.Map<LocationVariable,Term> atPres,
                                   java.util.Map<LocationVariable,Term> atBefores,
                                   ImmutableList<PositionedString> originalClauses)
                            throws SLTranslationException

Throws:: SLTranslationException

translateBreaks

private java.util.Map<Label,Term> translateBreaks(IProgramMethod pm,
                                                  ProgramVariable selfVar,
                                                  ImmutableList<ProgramVariable> paramVars,
                                                  ProgramVariable resultVar,
                                                  ProgramVariable excVar,
                                                  java.util.Map<LocationVariable,Term> atPres,
                                                  java.util.Map<LocationVariable,Term> atBefores,
                                                  Behavior originalBehavior,
                                                  ImmutableList<PositionedString> originalClauses)
                                           throws SLTranslationException

Throws:: SLTranslationException

translateContinues

private java.util.Map<Label,Term> translateContinues(IProgramMethod pm,
                                                     ProgramVariable selfVar,
                                                     ImmutableList<ProgramVariable> paramVars,
                                                     ProgramVariable resultVar,
                                                     ProgramVariable excVar,
                                                     java.util.Map<LocationVariable,Term> atPres,
                                                     java.util.Map<LocationVariable,Term> atBefores,
                                                     Behavior originalBehavior,
                                                     ImmutableList<PositionedString> originalClauses)
                                              throws SLTranslationException

Throws:: SLTranslationException

translateReturns

private Term translateReturns(IProgramMethod pm,
                              ProgramVariable selfVar,
                              ImmutableList<ProgramVariable> paramVars,
                              ProgramVariable resultVar,
                              ProgramVariable excVar,
                              java.util.Map<LocationVariable,Term> atPres,
                              java.util.Map<LocationVariable,Term> atBefores,
                              Behavior originalBehavior,
                              ImmutableList<PositionedString> originalClauses)
                       throws SLTranslationException

Throws:: SLTranslationException

translateSignals

private Term translateSignals(IProgramMethod pm,
                              ProgramVariable selfVar,
                              ImmutableList<ProgramVariable> paramVars,
                              ProgramVariable resultVar,
                              ProgramVariable excVar,
                              java.util.Map<LocationVariable,Term> atPres,
                              java.util.Map<LocationVariable,Term> atBefores,
                              Behavior originalBehavior,
                              ImmutableList<PositionedString> originalClauses)
                       throws SLTranslationException

Throws:: SLTranslationException

translateSignalsOnly

private Term translateSignalsOnly(IProgramMethod pm,
                                  ProgramVariable excVar,
                                  Behavior originalBehavior,
                                  ImmutableList<PositionedString> originalClauses)
                           throws SLTranslationException

Throws:: SLTranslationException

translateEnsures

private Term translateEnsures(IProgramMethod pm,
                              ProgramVariable selfVar,
                              ImmutableList<ProgramVariable> paramVars,
                              ProgramVariable resultVar,
                              ProgramVariable excVar,
                              java.util.Map<LocationVariable,Term> atPres,
                              java.util.Map<LocationVariable,Term> atBefores,
                              Behavior originalBehavior,
                              ImmutableList<PositionedString> originalClauses)
                       throws SLTranslationException

Throws:: SLTranslationException

translateAccessible

private Term translateAccessible(IProgramMethod pm,
                                 ProgramVariable selfVar,
                                 ImmutableList<ProgramVariable> paramVars,
                                 java.util.Map<LocationVariable,Term> atPres,
                                 java.util.Map<LocationVariable,Term> atBefores,
                                 ImmutableList<PositionedString> originalClauses)
                          throws SLTranslationException

Throws:: SLTranslationException

translateAssignable

private Term translateAssignable(IProgramMethod pm,
                                 ProgramVariable selfVar,
                                 ImmutableList<ProgramVariable> paramVars,
                                 java.util.Map<LocationVariable,Term> atPres,
                                 java.util.Map<LocationVariable,Term> atBefores,
                                 ImmutableList<PositionedString> originalClauses)
                          throws SLTranslationException

Throws:: SLTranslationException

translateStrictlyPure

private boolean translateStrictlyPure(IProgramMethod pm,
                                      ProgramVariable selfVar,
                                      ImmutableList<ProgramVariable> paramVars,
                                      ImmutableList<PositionedString> assignableClauses)
                               throws SLTranslationException

Throws:: SLTranslationException

translateMeasuredBy

private Term translateMeasuredBy(IProgramMethod pm,
                                 ProgramVariable selfVar,
                                 ImmutableList<ProgramVariable> paramVars,
                                 ImmutableList<PositionedString> originalMeasuredBy)
                          throws SLTranslationException

Throws:: SLTranslationException

translateDecreases

private Term translateDecreases(IProgramMethod pm,
                                ProgramVariable selfVar,
                                ImmutableList<ProgramVariable> paramVars,
                                java.util.Map<LocationVariable,Term> atPres,
                                java.util.Map<LocationVariable,Term> atBefores,
                                ImmutableList<PositionedString> originalDecreases)
                         throws SLTranslationException

Throws:: SLTranslationException

generateName

private java.lang.String generateName(IProgramMethod pm,
                                      TextualJMLSpecCase textualSpecCase,
                                      Behavior originalBehavior)

generatePostCondition

private java.util.Map<LocationVariable,Term> generatePostCondition(ProgramVariableCollection progVars,
                                                                   JMLSpecFactory.ContractClauses clauses,
                                                                   Behavior originalBehavior)

generateRepresentsAxioms

private java.util.Map<LocationVariable,Term> generateRepresentsAxioms(ProgramVariableCollection progVars,
                                                                      JMLSpecFactory.ContractClauses clauses,
                                                                      Behavior originalBehavior)

createFunctionalOperationContracts

private ImmutableSet<Contract> createFunctionalOperationContracts(java.lang.String name,
                                                                  IProgramMethod pm,
                                                                  ProgramVariableCollection progVars,
                                                                  JMLSpecFactory.ContractClauses clauses,
                                                                  java.util.Map<LocationVariable,Term> posts,
                                                                  java.util.Map<LocationVariable,Term> axioms)

Generate functional operation contracts.

Parameters:: name - base name of the contract (does not have to be unique); pm - the IProgramMethod to which the contract belongs; progVars - pre-generated collection of variables for the receiver object, operation parameters, operation result, thrown exception and the pre-heap; clauses - pre-translated JML clauses; post - pre-generated post condition
Returns:: operation contracts including new functional operation contracts

createDependencyOperationContract

private ImmutableSet<Contract> createDependencyOperationContract(IProgramMethod pm,
                                                                 ProgramVariableCollection progVars,
                                                                 JMLSpecFactory.ContractClauses clauses)

Generate dependency operation contract out of the JML accessible clause.

Parameters:: pm - the IProgramMethod to which the contract belongs; progVars - collection of variables for the receiver object, operation parameters, operation result, thrown exception and the pre-heap; clauses - pre-translated JML clauses
Returns:: operation contracts including a new dependency contract

createJMLClassInvariant

public ClassInvariant createJMLClassInvariant(KeYJavaType kjt,
                                              VisibilityModifier visibility,
                                              boolean isStatic,
                                              PositionedString originalInv)
                                       throws SLTranslationException

Throws:: SLTranslationException

createJMLClassInvariant

public ClassInvariant createJMLClassInvariant(KeYJavaType kjt,
                                              TextualJMLClassInv textualInv)
                                       throws SLTranslationException

Throws:: SLTranslationException

createJMLInitiallyClause

public InitiallyClause createJMLInitiallyClause(KeYJavaType kjt,
                                                VisibilityModifier visibility,
                                                PositionedString original)
                                         throws SLTranslationException

Throws:: SLTranslationException

createJMLInitiallyClause

public InitiallyClause createJMLInitiallyClause(KeYJavaType kjt,
                                                TextualJMLInitially textualInv)
                                         throws SLTranslationException

Throws:: SLTranslationException

createJMLRepresents

public ClassAxiom createJMLRepresents(KeYJavaType kjt,
                                      VisibilityModifier visibility,
                                      PositionedString originalRep,
                                      boolean isStatic)
                               throws SLTranslationException

Throws:: SLTranslationException

createJMLRepresents

public ClassAxiom createJMLRepresents(KeYJavaType kjt,
                                      TextualJMLRepresents textualRep)
                               throws SLTranslationException

Throws:: SLTranslationException

createJMLClassAxiom
```
public ClassAxiom createJMLClassAxiom(KeYJavaType kjt,
                                      TextualJMLClassAxiom textual)
                               throws SLTranslationException
```
Creates a class axiom from a textual JML representation. As JML axioms are always without modifiers, they are implicitly non-static and public.

Parameters:

kjt - the type where the axiom is declared

textual - textual representation

Returns:

created ClassAxiom

Throws:

SLTranslationException - translation exception

createJMLDependencyContract

public Contract createJMLDependencyContract(KeYJavaType kjt,
                                            LocationVariable targetHeap,
                                            PositionedString originalDep)
                                     throws SLTranslationException

Throws:: SLTranslationException

createJMLDependencyContract

public Contract createJMLDependencyContract(KeYJavaType kjt,
                                            TextualJMLDepends textualDep)
                                     throws SLTranslationException

Throws:: SLTranslationException

createJMLOperationContracts

public ImmutableSet<Contract> createJMLOperationContracts(IProgramMethod pm,
                                                          TextualJMLSpecCase textualSpecCase)
                                                   throws SLTranslationException

Creates operation contracts out of the passed JML specification.

Parameters:: pm - corresponding program method; textualSpecCase - textual representation of spec
Returns:: created JML operation contracts
Throws:: SLTranslationException - a translation exception

createJMLMergeContracts

public ImmutableSet<MergeContract> createJMLMergeContracts(IProgramMethod method,
                                                           MergePointStatement mps,
                                                           TextualJMLMergePointDecl mergePointDecl,
                                                           ImmutableList<ProgramVariable> methodParams)
                                                    throws SLTranslationException

Throws:: SLTranslationException

createJMLBlockContracts

public ImmutableSet<BlockContract> createJMLBlockContracts(IProgramMethod method,
                                                           java.util.List<Label> labels,
                                                           StatementBlock block,
                                                           TextualJMLSpecCase specificationCase)
                                                    throws SLTranslationException

Creates a set of block contracts for a block from a textual specification case.

Parameters:: method - the method containing the block.; labels - all labels belonging to the block.; block - the block which the block contracts belong to.; specificationCase - the textual specification case.
Returns:: a set of block contracts for a block from a textual specification case.
Throws:: SLTranslationException - translation exception

createJMLLoopContracts

public ImmutableSet<LoopContract> createJMLLoopContracts(IProgramMethod method,
                                                         java.util.List<Label> labels,
                                                         LoopStatement loop,
                                                         TextualJMLSpecCase specificationCase)
                                                  throws SLTranslationException

Creates a set of loop contracts for a loop from a textual specification case.

Parameters:: method - the method containing the block.; labels - all labels belonging to the block.; loop - the loop which the loop contracts belong to.; specificationCase - the textual specification case.
Returns:: a set of loop contracts for a block from a textual specification case.
Throws:: SLTranslationException - a translation exception

createJMLLoopContracts

public ImmutableSet<LoopContract> createJMLLoopContracts(IProgramMethod method,
                                                         java.util.List<Label> labels,
                                                         StatementBlock block,
                                                         TextualJMLSpecCase specificationCase)
                                                  throws SLTranslationException

Creates a set of loop contracts for a block from a textual specification case.

Parameters:: method - the method containing the block.; labels - all labels belonging to the block.; block - the block which the loop contracts belong to.; specificationCase - the textual specification case.
Returns:: a set of loop contracts for a block from a textual specification case.
Throws:: SLTranslationException - a translation exception

createProgramVariables

private ProgramVariableCollection createProgramVariables(IProgramMethod method,
                                                         JavaStatement block,
                                                         AuxiliaryContract.Variables variables)

Creates a program variable collection for a specified block. This collection contains all program variables that occur freely in the block as parameters (i.e., in ProgramVariableCollection.paramVars).

Parameters:: method - the method containing the block.; block - the block.; variables - an instance of AuxiliaryContract.Variables for the block.
Returns:

termify

private java.util.Map<LocationVariable,Term> termify(java.util.Map<LocationVariable,LocationVariable> remembranceVariables)

collectLocalVariablesVisibleTo

protected ImmutableList<ProgramVariable> collectLocalVariablesVisibleTo(Statement statement,
                                                                        IProgramMethod method)

collectLocalVariablesVisibleTo

private ImmutableList<ProgramVariable> collectLocalVariablesVisibleTo(Statement statement,
                                                                      StatementContainer container)

createJMLLoopInvariant

private LoopSpecification createJMLLoopInvariant(IProgramMethod pm,
                                                 LoopStatement loop,
                                                 java.util.Map<java.lang.String,ImmutableList<PositionedString>> originalInvariants,
                                                 java.util.Map<java.lang.String,ImmutableList<PositionedString>> originalFreeInvariants,
                                                 java.util.Map<java.lang.String,ImmutableList<PositionedString>> originalAssignables,
                                                 ImmutableList<PositionedString> originalInfFlowSpecs,
                                                 PositionedString originalVariant)
                                          throws SLTranslationException

Throws:: SLTranslationException

translateToTermVariant

private Term translateToTermVariant(IProgramMethod pm,
                                    ProgramVariable selfVar,
                                    java.util.Map<LocationVariable,Term> atPres,
                                    ImmutableList<ProgramVariable> allVars,
                                    PositionedString originalVariant)
                             throws SLTranslationException

Throws:: SLTranslationException

translateToTermInfFlowSpecs

private java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> translateToTermInfFlowSpecs(IProgramMethod pm,
                                                                                               ProgramVariable selfVar,
                                                                                               ProgramVariable resultVar,
                                                                                               ProgramVariable excVar,
                                                                                               ImmutableList<ProgramVariable> allVars,
                                                                                               ImmutableList<LocationVariable> allHeaps,
                                                                                               ImmutableList<PositionedString> originalInfFlowSpecs)
                                                                                        throws SLTranslationException

Throws:: SLTranslationException

translateToTermAsssignable

private java.util.Map<LocationVariable,Term> translateToTermAsssignable(IProgramMethod pm,
                                                                        ProgramVariable selfVar,
                                                                        java.util.Map<LocationVariable,Term> atPres,
                                                                        ImmutableList<ProgramVariable> allVars,
                                                                        java.util.Map<java.lang.String,ImmutableList<PositionedString>> originalAssignables)
                                                                 throws SLTranslationException

Throws:: SLTranslationException

append

private ImmutableList<ProgramVariable> append(ImmutableList<ProgramVariable> localVars,
                                              ImmutableList<LocationVariable> paramVars)

createJMLLoopInvariant

public LoopSpecification createJMLLoopInvariant(IProgramMethod pm,
                                                LoopStatement loop,
                                                TextualJMLLoopSpec textualLoopSpec)
                                         throws SLTranslationException

Throws:: SLTranslationException

initiallyClauseToContract
```
public FunctionalOperationContract initiallyClauseToContract(InitiallyClause ini,
                                                             IProgramMethod pm)
                                                      throws SLTranslationException
```
Translate initially clause to a contract for the given constructor. Exception is thrown if the methods passed is not a constructor. For an initially clause ini the resulting contract looks like:
requires true; ensures ini; signals (Exception) ini; diverges true;

Parameters:

ini - initially clause

pm - constructor

Returns:

the translated (functional operation) contract

Throws:

SLTranslationException - a translation exception

createPrecond

private ImmutableList<PositionedString> createPrecond(IProgramMethod pm,
                                                      PositionedString originalSpec)

Class JMLSpecFactory

Nested Class Summary

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

tb

services

cf

invCounter

modelFields

Constructor Detail

JMLSpecFactory

Method Detail

createAtPres

translateToTermInvariants

translateToTermFreeInvariants

createInformationFlowContracts

getDefaultInvName

getInicName

getContractName

collectLocalVariables

getVisibility

createProgramVariables

translateJMLClauses

translateAccessible

translateAxioms

translateEnsures

translateRequires

translateAssignable

registerAbbreviationVariables

translateInfFlowSpecClauses

translateAndClauses

translateOrClauses

translateUnionClauses

translateBreaks

translateContinues

translateReturns

translateSignals

translateSignalsOnly

translateEnsures

translateAccessible

translateAssignable

translateStrictlyPure

translateMeasuredBy

translateDecreases

generateName

generatePostCondition

generateRepresentsAxioms

createFunctionalOperationContracts

createDependencyOperationContract

createJMLClassInvariant

createJMLClassInvariant

createJMLInitiallyClause

createJMLInitiallyClause

createJMLRepresents

createJMLRepresents

createJMLClassAxiom

createJMLDependencyContract

createJMLDependencyContract

createJMLOperationContracts

createJMLMergeContracts

createJMLBlockContracts

createJMLLoopContracts

createJMLLoopContracts

createProgramVariables

termify

collectLocalVariablesVisibleTo

collectLocalVariablesVisibleTo

createJMLLoopInvariant

translateToTermVariant

translateToTermInfFlowSpecs

translateToTermAsssignable

append

createJMLLoopInvariant

initiallyClauseToContract

createPrecond