diff --git a/vdmj/documentation/MESSAGES b/vdmj/documentation/MESSAGES index b90a69b26..2012f206e 100644 --- a/vdmj/documentation/MESSAGES +++ b/vdmj/documentation/MESSAGES @@ -400,12 +400,14 @@ as the expected and actual values. 2327, "Type set1 is not available in classic" 2328, "Sequence binds are not available in classic" 2329, "Duplicate keyword" -2330, "Tokens found after expression at " +2330, "POG: Tokens found after obligation at " 2331, "Expecting inv, eq or ord clause" 2332, "Duplicate inv clause" 2333, "Type eq/ord clauses not available in classic" 2334, "Failed to instantiate ASTAnnotation" 2335, "Maximal '!' not allowed here" +2336, "POG: Obligation is not boolean?" +2337, "POG Obligation has type errors?" 3000, "Expression does not match declared type" diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedExpression.java index 72da7110c..c69fdda17 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedExpression.java @@ -28,6 +28,7 @@ import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -53,10 +54,10 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { annotation.poBefore(this, ctxt); - ProofObligationList obligations = expression.getProofObligations(ctxt, env); + ProofObligationList obligations = expression.getProofObligations(ctxt, pogState, env); annotation.poAfter(this, obligations, ctxt); return obligations; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POAssignmentDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POAssignmentDefinition.java index 105e2c48b..818aedd30 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POAssignmentDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POAssignmentDefinition.java @@ -70,7 +70,7 @@ public TCType getType() public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList obligations = new ProofObligationList(); - obligations.addAll(expression.getProofObligations(ctxt, env)); + obligations.addAll(expression.getProofObligations(ctxt, pogState, env)); obligations.stateUpdate(pogState, expression); if (!TypeComparator.isSubType(ctxt.checkType(expression, expType), type)) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassDefinition.java index cac218ad7..69762ff46 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassDefinition.java @@ -28,6 +28,7 @@ import com.fujitsu.vdmj.po.definitions.visitors.PODefinitionVisitor; import com.fujitsu.vdmj.po.statements.POClassInvariantStatement; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.definitions.TCClassDefinition; import com.fujitsu.vdmj.tc.lex.TCNameToken; @@ -172,14 +173,19 @@ public boolean hasNew() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment publicEnv) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment publicEnv) { ProofObligationList list = (annotations != null) ? annotations.poBefore(this) : new ProofObligationList(); Environment env = new PrivateClassEnvironment(tcdef, publicEnv); Environment local = new FlatEnvironment(tcdef.getSelfDefinition(), env); - list.addAll(definitions.getProofObligations(ctxt, local)); + + for (PODefinition def: definitions) + { + list.addAll(def.getProofObligations(new POContextStack(), new POGState(), local)); + } + list.typeCheck(tcdef.name, local); if (annotations != null) annotations.poAfter(this, list); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassInvariantDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassInvariantDefinition.java index de41939a1..b1b7eee80 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassInvariantDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassInvariantDefinition.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.po.definitions.visitors.PODefinitionVisitor; import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.StateInvariantObligation; @@ -63,7 +64,7 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList list = new ProofObligationList(); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassList.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassList.java index e7b27b508..68b642c04 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassList.java @@ -26,6 +26,7 @@ import com.fujitsu.vdmj.po.POMappedList; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.definitions.TCClassDefinition; import com.fujitsu.vdmj.tc.definitions.TCClassList; @@ -72,7 +73,7 @@ public ProofObligationList getProofObligations() for (POClassDefinition c: this) { - obligations.addAll(c.getProofObligations(new POContextStack(), new PublicClassEnvironment(tcclasses))); + obligations.addAll(c.getProofObligations(new POContextStack(), new POGState(), new PublicClassEnvironment(tcclasses))); } return obligations; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinition.java index 715a35bd8..eac306047 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinition.java @@ -130,22 +130,6 @@ public final TCNameList getVariableNames() list.addAll(apply(new POGetVariableNamesVisitor(), null)); return list; } - - /** - * True, if the definition contains executable statements that update state. - */ - public boolean updatesState() - { - return false; - } - - /** - * True, if the definition contains executable statements that read state. - */ - public boolean readsState() - { - return false; - } /** * Return the static type of the definition. For example, the type of a @@ -162,21 +146,15 @@ public boolean readsState() abstract public TCType getType(); /** - * Get a list of proof obligations for the definition. The second method is used - * to track the POG state for updates to state variables, which is only used - * by a few definition types (eg. POAssignmentDefinitions). + * Get a list of proof obligations for the definition. * * @param ctxt The call context. + * @param pogState Tracks updates to state in operations. * @return A list of POs. */ - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) - { - return new ProofObligationList(); - } - public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return getProofObligations(ctxt, env); // Default to stateless version + return new ProofObligationList(); } /** diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinitionList.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinitionList.java index 75a21e371..041d32956 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinitionList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinitionList.java @@ -28,7 +28,6 @@ import com.fujitsu.vdmj.pog.POContextStack; import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.POLetDefContext; -import com.fujitsu.vdmj.pog.PONameContext; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.definitions.TCDefinition; import com.fujitsu.vdmj.tc.definitions.TCDefinitionList; @@ -73,23 +72,6 @@ public String toString() return sb.toString(); } - /** - * Get the proof obligations from every definition in the list. - */ - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) - { - ProofObligationList obligations = new ProofObligationList(); - - for (PODefinition d: this) - { - ctxt.push(new PONameContext(d.getVariableNames())); - obligations.addAll(d.getProofObligations(ctxt, env)); - ctxt.pop(); - } - - return obligations; - } - /** * Get the proof obligations from every definition in the list and track POGState. */ @@ -110,7 +92,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog * one. This is used in let/def expressions, where definitions can depend on * earlier definitions in the same expression. */ - public ProofObligationList getDefProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getDefProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList obligations = new ProofObligationList(); int count = 0; @@ -120,9 +102,7 @@ public ProofObligationList getDefProofObligations(POContextStack ctxt, Environme ctxt.push(new POLetDefContext(d)); // In scope for recursive or total obligations count++; - ctxt.push(new PONameContext(d.getVariableNames())); - obligations.addAll(d.getProofObligations(ctxt, env)); - ctxt.pop(); + obligations.addAll(d.getProofObligations(ctxt, pogState, env)); } for (int i=0; i R apply(PODefinitionVisitor visitor, S arg) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitFunctionDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitFunctionDefinition.java index de1724377..89f6e687b 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitFunctionDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitFunctionDefinition.java @@ -38,6 +38,7 @@ import com.fujitsu.vdmj.pog.POContextStack; import com.fujitsu.vdmj.pog.POFunctionDefinitionContext; import com.fujitsu.vdmj.pog.POFunctionResultContext; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.PONameContext; import com.fujitsu.vdmj.pog.ParameterPatternObligation; import com.fujitsu.vdmj.pog.ProofObligationList; @@ -128,7 +129,7 @@ public TCType getType() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList obligations = (annotations != null) ? annotations.poBefore(this, ctxt) : new ProofObligationList(); @@ -155,7 +156,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment if (precondition != null) { - obligations.addAll(predef.getProofObligations(ctxt, env)); + obligations.addAll(predef.getProofObligations(ctxt, pogState, env)); } if (postcondition != null) @@ -171,7 +172,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment { ctxt.push(new POFunctionDefinitionContext(this, false)); ctxt.push(new POFunctionResultContext(this)); - obligations.addAll(postcondition.getProofObligations(ctxt, env)); + obligations.addAll(postcondition.getProofObligations(ctxt, pogState, env)); ctxt.pop(); ctxt.pop(); } @@ -180,7 +181,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment if (measureDef != null && measureName != null && measureName.isMeasureName()) { ctxt.push(new PONameContext(new TCNameList(measureName))); - obligations.addAll(measureDef.getProofObligations(ctxt, env)); + obligations.addAll(measureDef.getProofObligations(ctxt, pogState, env)); ctxt.pop(); } @@ -196,7 +197,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment else { ctxt.push(new POFunctionDefinitionContext(this, true)); - obligations.addAll(body.getProofObligations(ctxt, env)); + obligations.addAll(body.getProofObligations(ctxt, pogState, env)); if (isUndefined || !TypeComparator.isSubType(actualResult, type.result)) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitOperationDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitOperationDefinition.java index 050655b17..72b68ad30 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitOperationDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitOperationDefinition.java @@ -133,7 +133,7 @@ public TCType getType() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList obligations = (annotations != null) ? annotations.poBefore(this, ctxt) : new ProofObligationList(); @@ -165,7 +165,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment */ if (precondition != null && Settings.dialect == Dialect.VDM_SL) { - obligations.addAll(predef.getProofObligations(ctxt, env)); + obligations.addAll(predef.getProofObligations(ctxt, pogState, env)); } if (postcondition != null && Settings.dialect == Dialect.VDM_SL) @@ -180,7 +180,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment } else { - obligations.addAll(postdef.getProofObligations(ctxt, env)); + obligations.addAll(postdef.getProofObligations(ctxt, pogState, env)); } obligations.add(new OperationPostConditionObligation(this, ctxt)); @@ -188,18 +188,16 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment if (body != null) { - POGState pstate = new POGState(); - if (stateDefinition != null) { ctxt.push(new POOperationDefinitionContext(this, (precondition != null), stateDefinition, true)); - obligations.addAll(body.getProofObligations(ctxt, pstate, env)); + obligations.addAll(body.getProofObligations(ctxt, pogState, env)); ctxt.pop(); } else if (classDefinition != null) { ctxt.push(new POOperationDefinitionContext(this, (precondition != null), classDefinition, true)); - ProofObligationList oblist = body.getProofObligations(ctxt, pstate, env); + ProofObligationList oblist = body.getProofObligations(ctxt, pogState, env); ctxt.pop(); if (Settings.release != Release.VDM_10) // Uses the obj_C pattern in OperationDefContext @@ -216,7 +214,7 @@ else if (precondition != null) // pre_op state param undefined in VDM++ else // Flat spec with no state defined { ctxt.push(new POOperationDefinitionContext(this, (precondition != null), null, true)); - obligations.addAll(body.getProofObligations(ctxt, pstate, env)); + obligations.addAll(body.getProofObligations(ctxt, pogState, env)); ctxt.pop(); } @@ -272,18 +270,6 @@ public POPatternList getParamPatternList() return plist; } - - @Override - public boolean updatesState() - { - return body == null ? false : body.updatesState(); - } - - @Override - public boolean readsState() - { - return body == null ? false : body.readsState(); - } @Override public R apply(PODefinitionVisitor visitor, S arg) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POPerSyncDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POPerSyncDefinition.java index c244d6271..bc9f3e340 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POPerSyncDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POPerSyncDefinition.java @@ -29,6 +29,7 @@ import com.fujitsu.vdmj.po.definitions.visitors.PODefinitionVisitor; import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.PONameContext; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.lex.TCNameList; @@ -64,13 +65,13 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList obligations = (annotations != null) ? annotations.poBefore(this, ctxt) : new ProofObligationList(); ctxt.push(new PONameContext(new TCNameList(opname))); - obligations.addAll(guard.getProofObligations(ctxt, env)); + obligations.addAll(guard.getProofObligations(ctxt, pogState, env)); ctxt.pop(); if (annotations != null) annotations.poAfter(this, obligations, ctxt); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POQualifiedDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POQualifiedDefinition.java index 864e24abb..b55faafaf 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POQualifiedDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POQualifiedDefinition.java @@ -26,6 +26,7 @@ import com.fujitsu.vdmj.po.definitions.visitors.PODefinitionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.typechecker.Environment; @@ -75,9 +76,9 @@ public TCType getType() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return def.getProofObligations(ctxt, env); + return def.getProofObligations(ctxt, pogState, env); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POStateDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POStateDefinition.java index 2622c3801..4249be8bb 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POStateDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POStateDefinition.java @@ -28,6 +28,7 @@ import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.po.patterns.POPattern; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.PONameContext; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.SatisfiabilityObligation; @@ -111,7 +112,7 @@ public TCType getType() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList list = (annotations != null) ? annotations.poBefore(this, ctxt) : new ProofObligationList(); @@ -121,13 +122,13 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment if (invExpression != null) { - list.addAll(invdef.getProofObligations(ctxt, env)); + list.addAll(invdef.getProofObligations(ctxt, pogState, env)); list.add(new SatisfiabilityObligation(this, ctxt)); } if (initExpression != null) { - list.addAll(initdef.getProofObligations(ctxt, env)); + list.addAll(initdef.getProofObligations(ctxt, pogState, env)); list.add(new StateInitObligation(this, ctxt)); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POTypeDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POTypeDefinition.java index 9e9b17334..4fbadb891 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POTypeDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POTypeDefinition.java @@ -30,6 +30,7 @@ import com.fujitsu.vdmj.po.patterns.POPattern; import com.fujitsu.vdmj.pog.EquivRelationObligation; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.SatisfiabilityObligation; import com.fujitsu.vdmj.pog.StrictOrderObligation; @@ -102,26 +103,26 @@ public TCType getType() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList list = (annotations != null) ? annotations.poBefore(this, ctxt) : new ProofObligationList(); if (invdef != null) { - list.addAll(invdef.getProofObligations(ctxt, env)); + list.addAll(invdef.getProofObligations(ctxt, pogState, env)); list.add(new SatisfiabilityObligation(this, ctxt)); } if (eqdef != null) { - list.addAll(eqdef.getProofObligations(ctxt, env)); + list.addAll(eqdef.getProofObligations(ctxt, pogState, env)); list.add(new EquivRelationObligation(this, ctxt)); } if (orddef != null) { - list.addAll(orddef.getProofObligations(ctxt, env)); + list.addAll(orddef.getProofObligations(ctxt, pogState, env)); list.add(new StrictOrderObligation(this, ctxt)); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POValueDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POValueDefinition.java index 7f0baeb81..8c48100d4 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POValueDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POValueDefinition.java @@ -32,6 +32,7 @@ import com.fujitsu.vdmj.po.patterns.POIgnorePattern; import com.fujitsu.vdmj.po.patterns.POPattern; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.SubTypeObligation; import com.fujitsu.vdmj.pog.ValueBindingObligation; @@ -103,12 +104,13 @@ public TCType getType() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList list = (annotations != null) ? annotations.poBefore(this, ctxt) : new ProofObligationList(); - list.addAll(exp.getProofObligations(ctxt, env)); + list.addAll(exp.getProofObligations(ctxt, pogState, env)); + list.stateUpdate(pogState, exp); if (!(pattern instanceof POIdentifierPattern) && !(pattern instanceof POIgnorePattern) && diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POAndExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POAndExpression.java index f6685e215..621878e9c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POAndExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POAndExpression.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.ast.lex.LexToken; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.POImpliesContext; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.SubTypeObligation; @@ -45,7 +46,7 @@ public POAndExpression(POExpression left, LexToken op, POExpression right, } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList obligations = new ProofObligationList(); @@ -63,10 +64,10 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment ctxt.pop(); } - obligations.addAll(left.getProofObligations(ctxt, env)); + obligations.addAll(left.getProofObligations(ctxt, pogState, env)); ctxt.push(new POImpliesContext(left)); - obligations.addAll(right.getProofObligations(ctxt, env)); + obligations.addAll(right.getProofObligations(ctxt, pogState, env)); ctxt.pop(); return obligations; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java index da730d494..e51c34529 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java @@ -30,6 +30,7 @@ import com.fujitsu.vdmj.pog.FunctionApplyObligation; import com.fujitsu.vdmj.pog.MapApplyObligation; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.RecursiveObligation; import com.fujitsu.vdmj.pog.SeqApplyObligation; @@ -84,76 +85,83 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList obligations = new ProofObligationList(); - if (!type.isUnknown(location) && type.isMap(location)) + if (!type.isUnknown(location)) { - TCMapType m = type.getMap(); - obligations.add(new MapApplyObligation(root, args.get(0), ctxt)); - TCType atype = ctxt.checkType(args.get(0), argtypes.get(0)); - - if (!TypeComparator.isSubType(atype, m.from)) + if (type.isOperation(location)) { - obligations.add(new SubTypeObligation(args.get(0), m.from, atype, ctxt)); + pogState.didUpdateState(); // Operation calls assumed to update state } - } - - if (!type.isUnknown(location) && - (type.isFunction(location) || type.isOperation(location))) - { - String prename = root.getPreName(); - if (type.isFunction(location) && prename != null && !prename.isEmpty()) + if (type.isMap(location)) { - obligations.add(new FunctionApplyObligation(root, args, prename, ctxt)); + TCMapType m = type.getMap(); + obligations.add(new MapApplyObligation(root, args.get(0), ctxt)); + TCType atype = ctxt.checkType(args.get(0), argtypes.get(0)); + + if (!TypeComparator.isSubType(atype, m.from)) + { + obligations.add(new SubTypeObligation(args.get(0), m.from, atype, ctxt)); + } } - - TCTypeList paramTypes = type.isFunction(location) ? - type.getFunction().parameters : type.getOperation().parameters; - - int i=0; - - for (TCType at: argtypes) + + if (type.isFunction(location) || type.isOperation(location)) { - at = ctxt.checkType(args.get(i), at); - TCType pt = paramTypes.get(i); - - if (!TypeComparator.isSubType(at, pt)) + String prename = root.getPreName(); + + if (type.isFunction(location) && prename != null && !prename.isEmpty()) { - obligations.add(new SubTypeObligation(args.get(i), pt, at, ctxt)); + obligations.add(new FunctionApplyObligation(root, args, prename, ctxt)); + } + + TCTypeList paramTypes = type.isFunction(location) ? + type.getFunction().parameters : type.getOperation().parameters; + + int i=0; + + for (TCType at: argtypes) + { + at = ctxt.checkType(args.get(i), at); + TCType pt = paramTypes.get(i); + + if (!TypeComparator.isSubType(at, pt)) + { + obligations.add(new SubTypeObligation(args.get(i), pt, at, ctxt)); + } + + i++; } - - i++; } - } - - if (!type.isUnknown(location) && type.isFunction(location)) - { - if (recursiveCycles != null) // name is a function in a recursive loop + + if (type.isFunction(location)) { - /** - * All of the functions in the loop will generate similar obligations, - * so the "add" method eliminates any duplicates. - */ - for (PODefinitionList loop: recursiveCycles) + if (recursiveCycles != null) // name is a function in a recursive loop { - obligations.add(new RecursiveObligation(location, loop, this, ctxt)); + /** + * All of the functions in the loop will generate similar obligations, + * so the "add" method eliminates any duplicates. + */ + for (PODefinitionList loop: recursiveCycles) + { + obligations.add(new RecursiveObligation(location, loop, this, ctxt)); + } } } + + if (type.isSeq(location)) + { + obligations.add(new SeqApplyObligation(root, args.get(0), ctxt)); + } } - if (!type.isUnknown(location) && type.isSeq(location)) - { - obligations.add(new SeqApplyObligation(root, args.get(0), ctxt)); - } - - obligations.addAll(root.getProofObligations(ctxt, env)); + obligations.addAll(root.getProofObligations(ctxt, pogState, env)); for (POExpression arg: args) { - obligations.addAll(arg.getProofObligations(ctxt, env)); + obligations.addAll(arg.getProofObligations(ctxt, pogState, env)); } return obligations; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POBinaryExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POBinaryExpression.java index 76c69b9a0..047178709 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POBinaryExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POBinaryExpression.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.ast.lex.LexToken; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.tc.types.TCTypeQualifier; @@ -54,11 +55,11 @@ public POBinaryExpression(POExpression left, LexToken op, POExpression right, } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList obligations = new ProofObligationList(); - obligations.addAll(left.getProofObligations(ctxt, env)); - obligations.addAll(right.getProofObligations(ctxt, env)); + obligations.addAll(left.getProofObligations(ctxt, pogState, env)); + obligations.addAll(right.getProofObligations(ctxt, pogState, env)); obligations.addAll(checkUnionQualifiers(left, getLeftQualifier(), ctxt)); obligations.addAll(checkUnionQualifiers(right, getRightQualifier(), ctxt)); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POBooleanBinaryExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POBooleanBinaryExpression.java index ed34aa7aa..ef64145b7 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POBooleanBinaryExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POBooleanBinaryExpression.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.ast.lex.LexToken; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.SubTypeObligation; import com.fujitsu.vdmj.tc.types.TCBooleanType; @@ -45,9 +46,9 @@ public POBooleanBinaryExpression(POExpression left, LexToken op, POExpression ri } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList obligations = super.getProofObligations(ctxt, env); + ProofObligationList obligations = super.getProofObligations(ctxt, pogState, env); if (ltype.isUnion(location)) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POCaseAlternative.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POCaseAlternative.java index 6c51a4032..e187fbbe0 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POCaseAlternative.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POCaseAlternative.java @@ -29,6 +29,7 @@ import com.fujitsu.vdmj.po.patterns.POPattern; import com.fujitsu.vdmj.pog.POCaseContext; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.PONotCaseContext; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCType; @@ -57,12 +58,12 @@ public String toString() return pattern + " -> " + result; } - public ProofObligationList getProofObligations(POContextStack ctxt, TCType type, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, TCType type, Environment env) { ProofObligationList obligations = new ProofObligationList(); ctxt.push(new POCaseContext(pattern, type, cexp)); - obligations.addAll(result.getProofObligations(ctxt, env)); + obligations.addAll(result.getProofObligations(ctxt, pogState, env)); ctxt.pop(); ctxt.push(new PONotCaseContext(pattern, type, cexp)); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POCasesExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POCasesExpression.java index 8c4e8c737..f1c740003 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POCasesExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POCasesExpression.java @@ -29,6 +29,7 @@ import com.fujitsu.vdmj.po.patterns.POIgnorePattern; import com.fujitsu.vdmj.pog.CasesExhaustiveObligation; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.lex.TCNameList; @@ -63,9 +64,9 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList obligations = exp.getProofObligations(ctxt, env); + ProofObligationList obligations = exp.getProofObligations(ctxt, pogState, env); boolean hasIgnore = false; TCNameList hidden = new TCNameList(); @@ -81,12 +82,12 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment hidden.addAll(alt.pattern.getHiddenVariables()); // cumulative // PONotCaseContext pushed by the POCaseAlternative... - _obligations.addAll(alt.getProofObligations(ctxt, expType, env)); + _obligations.addAll(alt.getProofObligations(ctxt, pogState, expType, env)); } if (others != null) { - _obligations.addAll(others.getProofObligations(ctxt, env)); + _obligations.addAll(others.getProofObligations(ctxt, pogState, env)); } for (int i=0; i for (POElseIfExpression exp: elseList) { - obligations.addAll(exp.getProofObligations(ctxt, env)); + obligations.addAll(exp.getProofObligations(ctxt, pogState, env)); ctxt.push(new PONotImpliesContext(exp.elseIfExp)); } - obligations.addAll(elseExp.getProofObligations(ctxt, env)); + obligations.addAll(elseExp.getProofObligations(ctxt, pogState, env)); for (int i=0; i 1) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMapInverseExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMapInverseExpression.java index 3d337f9c5..e92d4ba43 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMapInverseExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMapInverseExpression.java @@ -28,6 +28,7 @@ import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.InvariantObligation; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCMapType; import com.fujitsu.vdmj.tc.types.TCTypeQualifier; @@ -51,9 +52,9 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList list = super.getProofObligations(ctxt, env); + ProofObligationList list = super.getProofObligations(ctxt, pogState, env); if (!type.empty) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMapUnionExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMapUnionExpression.java index f3146b087..43a9d1d4c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMapUnionExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMapUnionExpression.java @@ -28,6 +28,7 @@ import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.MapCompatibleObligation; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.tc.types.TCTypeQualifier; @@ -44,9 +45,9 @@ public POMapUnionExpression(POExpression left, LexToken op, POExpression right, } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList obligations = super.getProofObligations(ctxt, env); + ProofObligationList obligations = super.getProofObligations(ctxt, pogState, env); obligations.add(new MapCompatibleObligation(left, right, ctxt)); return obligations; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMapletExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMapletExpression.java index 4d2ecd5f2..c224c4f25 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMapletExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMapletExpression.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.PONode; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -51,10 +52,10 @@ public String toString() return left + " |-> " + right; } - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList list = left.getProofObligations(ctxt, env); - list.addAll(right.getProofObligations(ctxt, env)); + ProofObligationList list = left.getProofObligations(ctxt, pogState, env); + list.addAll(right.getProofObligations(ctxt, pogState, env)); return list; } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMkBasicExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMkBasicExpression.java index 6ef946d8f..26848bd39 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMkBasicExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMkBasicExpression.java @@ -26,6 +26,7 @@ import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.typechecker.Environment; @@ -50,9 +51,9 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return arg.getProofObligations(ctxt, env); + return arg.getProofObligations(ctxt, pogState, env); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMkTypeExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMkTypeExpression.java index 118073bb4..13514a9b0 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMkTypeExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMkTypeExpression.java @@ -28,6 +28,7 @@ import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.SubTypeObligation; import com.fujitsu.vdmj.tc.lex.TCNameToken; @@ -64,9 +65,9 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList list = args.getProofObligations(ctxt, env); + ProofObligationList list = args.getProofObligations(ctxt, pogState, env); Iterator it = argTypes.iterator(); int i = 0; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMuExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMuExpression.java index 40b71b3e7..b20e3f925 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMuExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMuExpression.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.SubTypeObligation; import com.fujitsu.vdmj.tc.types.TCField; @@ -62,14 +63,14 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList list = record.getProofObligations(ctxt, env); + ProofObligationList list = record.getProofObligations(ctxt, pogState, env); int i = 0; for (PORecordModifier rm: modifiers) { - list.addAll(rm.value.getProofObligations(ctxt, env)); + list.addAll(rm.value.getProofObligations(ctxt, pogState, env)); TCField f = recordType.findField(rm.tag.getName()); TCType mtype = modTypes.get(i++); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PONarrowExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PONarrowExpression.java index 0ff5d6c70..41dabec0b 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PONarrowExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PONarrowExpression.java @@ -28,6 +28,7 @@ import com.fujitsu.vdmj.po.definitions.PODefinition; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.SubTypeObligation; import com.fujitsu.vdmj.tc.lex.TCNameToken; @@ -62,7 +63,7 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList obligations = new ProofObligationList(); @@ -74,7 +75,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment obligations.add(new SubTypeObligation(test, expected, testtype, ctxt)); } - obligations.addAll(test.getProofObligations(ctxt, env)); + obligations.addAll(test.getProofObligations(ctxt, pogState, env)); return obligations; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PONewExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PONewExpression.java index 693e878b4..5e909df41 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PONewExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PONewExpression.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.lex.TCIdentifierToken; import com.fujitsu.vdmj.typechecker.Environment; @@ -52,9 +53,9 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return args.getProofObligations(ctxt, env); + return args.getProofObligations(ctxt, pogState, env); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PONumericBinaryExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PONumericBinaryExpression.java index 8b3d0b7f1..f4330bcb2 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PONumericBinaryExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PONumericBinaryExpression.java @@ -28,6 +28,7 @@ import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.OrderedObligation; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.SubTypeObligation; import com.fujitsu.vdmj.tc.types.TCOptionalType; @@ -48,9 +49,9 @@ public PONumericBinaryExpression(POExpression left, LexToken op, POExpression ri } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList obligations = super.getProofObligations(ctxt, env); + ProofObligationList obligations = super.getProofObligations(ctxt, pogState, env); obligations.addAll(getNonNilObligations(ctxt)); return obligations; } @@ -80,11 +81,11 @@ private ProofObligationList getNonNilObligations(POContextStack ctxt) /** * Generate ordering obligations, as used by the comparison operators. */ - protected ProofObligationList getOrderedObligations(POContextStack ctxt, Environment env) + protected ProofObligationList getOrderedObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList obligations = getCommonOrderedObligations(ctxt); - obligations.addAll(left.getProofObligations(ctxt, env)); - obligations.addAll(right.getProofObligations(ctxt, env)); + obligations.addAll(left.getProofObligations(ctxt, pogState, env)); + obligations.addAll(right.getProofObligations(ctxt, pogState, env)); return obligations; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POOrExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POOrExpression.java index ce238a96d..3b8be8fac 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POOrExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POOrExpression.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.ast.lex.LexToken; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.PONotImpliesContext; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.SubTypeObligation; @@ -45,7 +46,7 @@ public POOrExpression(POExpression left, LexToken op, POExpression right, } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList obligations = new ProofObligationList(); @@ -63,10 +64,10 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment ctxt.pop(); } - obligations.addAll(left.getProofObligations(ctxt, env)); + obligations.addAll(left.getProofObligations(ctxt, pogState, env)); ctxt.push(new PONotImpliesContext(left)); - obligations.addAll(right.getProofObligations(ctxt, env)); + obligations.addAll(right.getProofObligations(ctxt, pogState, env)); ctxt.pop(); return obligations; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POPlusPlusExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POPlusPlusExpression.java index 43508d483..2ec0d4fa4 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POPlusPlusExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POPlusPlusExpression.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.ast.lex.LexToken; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.SeqModificationObligation; import com.fujitsu.vdmj.tc.types.TCType; @@ -44,9 +45,9 @@ public POPlusPlusExpression(POExpression left, LexToken op, POExpression right, } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList obligations = super.getProofObligations(ctxt, env); + ProofObligationList obligations = super.getProofObligations(ctxt, pogState, env); if (ltype.isSeq(location)) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSameBaseClassExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSameBaseClassExpression.java index db7483d31..f76cde39e 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSameBaseClassExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSameBaseClassExpression.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -45,10 +46,10 @@ public POSameBaseClassExpression(LexLocation start, POExpression left, POExpress } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList list = left.getProofObligations(ctxt, env); - list.addAll(right.getProofObligations(ctxt, env)); + ProofObligationList list = left.getProofObligations(ctxt, pogState, env); + list.addAll(right.getProofObligations(ctxt, pogState, env)); return list; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSameClassExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSameClassExpression.java index e4e728353..de3c0a0f1 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSameClassExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSameClassExpression.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -45,10 +46,10 @@ public POSameClassExpression(LexLocation start, POExpression left, POExpression } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList list = left.getProofObligations(ctxt, env); - list.addAll(right.getProofObligations(ctxt, env)); + ProofObligationList list = left.getProofObligations(ctxt, pogState, env); + list.addAll(right.getProofObligations(ctxt, pogState, env)); return list; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSeqCompExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSeqCompExpression.java index 4c5fcf37e..b88912c34 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSeqCompExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSeqCompExpression.java @@ -28,6 +28,7 @@ import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.po.patterns.POBind; import com.fujitsu.vdmj.pog.POForAllPredicateContext; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.POForAllContext; import com.fujitsu.vdmj.pog.POContextStack; import com.fujitsu.vdmj.pog.ProofObligationList; @@ -58,20 +59,20 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList obligations = new ProofObligationList(); ctxt.push(new POForAllPredicateContext(this)); - obligations.addAll(first.getProofObligations(ctxt, env)); + obligations.addAll(first.getProofObligations(ctxt, pogState, env)); ctxt.pop(); - obligations.addAll(bind.getProofObligations(ctxt, env)); + obligations.addAll(bind.getProofObligations(ctxt, pogState, env)); if (predicate != null) { ctxt.push(new POForAllContext(this)); - obligations.addAll(predicate.getProofObligations(ctxt, env)); + obligations.addAll(predicate.getProofObligations(ctxt, pogState, env)); obligations.addAll(checkUnionQualifiers(predicate, TCTypeQualifier.getBoolQualifier(), ctxt)); ctxt.pop(); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSeqEnumExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSeqEnumExpression.java index 6478625c3..1fc078afb 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSeqEnumExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSeqEnumExpression.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCTypeList; import com.fujitsu.vdmj.typechecker.Environment; @@ -52,9 +53,9 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return members.getProofObligations(ctxt, env); + return members.getProofObligations(ctxt, pogState, env); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSetCompExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSetCompExpression.java index 058517f80..428b14476 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSetCompExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSetCompExpression.java @@ -33,6 +33,7 @@ import com.fujitsu.vdmj.pog.POContextStack; import com.fujitsu.vdmj.pog.POForAllContext; import com.fujitsu.vdmj.pog.POForAllPredicateContext; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCSetType; import com.fujitsu.vdmj.tc.types.TCTypeQualifier; @@ -65,19 +66,19 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList obligations = new ProofObligationList(); ctxt.push(new POForAllPredicateContext(this)); - obligations.addAll(first.getProofObligations(ctxt, env)); + obligations.addAll(first.getProofObligations(ctxt, pogState, env)); ctxt.pop(); boolean finiteTest = false; for (POMultipleBind mb: bindings) { - obligations.addAll(mb.getProofObligations(ctxt, env)); + obligations.addAll(mb.getProofObligations(ctxt, pogState, env)); if (mb instanceof POMultipleTypeBind) { @@ -93,7 +94,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment if (predicate != null) { ctxt.push(new POForAllContext(this)); - obligations.addAll(predicate.getProofObligations(ctxt, env)); + obligations.addAll(predicate.getProofObligations(ctxt, pogState, env)); obligations.addAll(checkUnionQualifiers(predicate, TCTypeQualifier.getBoolQualifier(), ctxt)); ctxt.pop(); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSetEnumExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSetEnumExpression.java index 77ca4af99..4e4a06e11 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSetEnumExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSetEnumExpression.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCTypeList; import com.fujitsu.vdmj.typechecker.Environment; @@ -52,9 +53,9 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return members.getProofObligations(ctxt, env); + return members.getProofObligations(ctxt, pogState, env); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSetRangeExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSetRangeExpression.java index 34256bf24..a755c6369 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSetRangeExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSetRangeExpression.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.tc.types.TCTypeQualifier; @@ -57,10 +58,10 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList obligations = first.getProofObligations(ctxt, env); - obligations.addAll(last.getProofObligations(ctxt, env)); + ProofObligationList obligations = first.getProofObligations(ctxt, pogState, env); + obligations.addAll(last.getProofObligations(ctxt, pogState, env)); obligations.addAll(checkUnionQualifiers(first, TCTypeQualifier.getNumericQualifier(), ctxt)); obligations.addAll(checkUnionQualifiers(last, TCTypeQualifier.getNumericQualifier(), ctxt)); return obligations; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POStarStarExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POStarStarExpression.java index d34c85b24..e322ba25c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POStarStarExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POStarStarExpression.java @@ -29,6 +29,7 @@ import com.fujitsu.vdmj.pog.FuncIterationObligation; import com.fujitsu.vdmj.pog.MapIterationObligation; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.tc.types.TCTypeQualifier; @@ -45,7 +46,7 @@ public POStarStarExpression(POExpression left, LexToken op, POExpression right, } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList obligations = new ProofObligationList(); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSubseqExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSubseqExpression.java index a355b5b09..9e2240cf1 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSubseqExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSubseqExpression.java @@ -26,6 +26,7 @@ import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.tc.types.TCTypeQualifier; @@ -58,11 +59,11 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList list = seq.getProofObligations(ctxt, env); - list.addAll(from.getProofObligations(ctxt, env)); - list.addAll(to.getProofObligations(ctxt, env)); + ProofObligationList list = seq.getProofObligations(ctxt, pogState, env); + list.addAll(from.getProofObligations(ctxt, pogState, env)); + list.addAll(to.getProofObligations(ctxt, pogState, env)); list.addAll(checkUnionQualifiers(from, TCTypeQualifier.getNumericQualifier(), ctxt)); list.addAll(checkUnionQualifiers(to, TCTypeQualifier.getNumericQualifier(), ctxt)); return list; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POTailExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POTailExpression.java index 1a65c21da..0e298a472 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POTailExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POTailExpression.java @@ -28,6 +28,7 @@ import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.NonEmptySeqObligation; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCSeq1Type; import com.fujitsu.vdmj.tc.types.TCType; @@ -52,9 +53,9 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList obligations = super.getProofObligations(ctxt, env); + ProofObligationList obligations = super.getProofObligations(ctxt, pogState, env); if (!etype.isAlways(TCSeq1Type.class, location)) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POTupleExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POTupleExpression.java index 362d9d2fe..ca7f7d4c5 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POTupleExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POTupleExpression.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCTypeList; import com.fujitsu.vdmj.typechecker.Environment; @@ -52,9 +53,9 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return args.getProofObligations(ctxt, env); + return args.getProofObligations(ctxt, pogState, env); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POUnaryExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POUnaryExpression.java index 2b3830fa7..e73e3f3be 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POUnaryExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POUnaryExpression.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.SubTypeObligation; import com.fujitsu.vdmj.tc.types.TCType; @@ -47,9 +48,9 @@ public POUnaryExpression(LexLocation location, POExpression exp) } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList list = exp.getProofObligations(ctxt, env); + ProofObligationList list = exp.getProofObligations(ctxt, pogState, env); if (exp.getExptype() != null && exp.getExptype().isUnion(location)) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/visitors/POExpressionStateFinder.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/visitors/POExpressionStateFinder.java index d5a1867bf..985c422b5 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/visitors/POExpressionStateFinder.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/visitors/POExpressionStateFinder.java @@ -25,10 +25,12 @@ package com.fujitsu.vdmj.po.expressions.visitors; import com.fujitsu.vdmj.po.POVisitorSet; +import com.fujitsu.vdmj.po.expressions.POApplyExpression; import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.po.expressions.POVariableExpression; import com.fujitsu.vdmj.tc.lex.TCNameSet; import com.fujitsu.vdmj.tc.lex.TCNameToken; +import com.fujitsu.vdmj.tc.types.TCOperationType; import com.fujitsu.vdmj.typechecker.NameScope; /** @@ -54,6 +56,23 @@ public TCNameSet caseVariableExpression(POVariableExpression node, Boolean updat return all; } + @Override + public TCNameSet caseApplyExpression(POApplyExpression node, Boolean updates) + { + TCNameSet all = super.caseApplyExpression(node, updates); + + if (node.type instanceof TCOperationType) + { + if (node.root instanceof POVariableExpression) + { + POVariableExpression name = (POVariableExpression)node.root; + all.add(name.name); + } + } + + return all; + } + @Override protected TCNameSet newCollection() { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/modules/POModule.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/modules/POModule.java index 3c17cc213..cc7e83b6a 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/modules/POModule.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/modules/POModule.java @@ -31,6 +31,8 @@ import com.fujitsu.vdmj.po.definitions.PODefinition; import com.fujitsu.vdmj.po.definitions.PODefinitionList; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; +import com.fujitsu.vdmj.pog.PONameContext; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.lex.TCIdentifierToken; import com.fujitsu.vdmj.tc.modules.TCModule; @@ -88,7 +90,14 @@ public ProofObligationList getProofObligations(MultiModuleEnvironment menv) ProofObligationList list = (annotations != null) ? annotations.poBefore(this) : new ProofObligationList(); - list.addAll(defs.getProofObligations(new POContextStack(), menv)); + for (PODefinition def: defs) + { + POContextStack ctxt = new POContextStack(); + ctxt.push(new PONameContext(def.getVariableNames())); + list.addAll(def.getProofObligations(ctxt, new POGState(), menv)); + ctxt.pop(); + } + list.typeCheck(tcmodule, menv); if (annotations != null) annotations.poAfter(this, list); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POBind.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POBind.java index 68cab131b..cc3f8ad1b 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POBind.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POBind.java @@ -31,6 +31,7 @@ import com.fujitsu.vdmj.po.PONode; import com.fujitsu.vdmj.po.patterns.visitors.POBindVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -57,7 +58,7 @@ public POBind(LexLocation location, POPattern pattern) abstract public List getMultipleBindList(); /** Return a list of POs. */ - abstract public ProofObligationList getProofObligations(POContextStack ctxt, Environment env); + abstract public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env); /** * Implemented by all binds to allow visitor processing. diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleBind.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleBind.java index abce9b694..d8c23cd72 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleBind.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleBind.java @@ -31,6 +31,7 @@ import com.fujitsu.vdmj.po.PONode; import com.fujitsu.vdmj.po.patterns.visitors.POMultipleBindVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -66,7 +67,7 @@ public List getMultipleBindList() } /** Get a list of POs. */ - abstract public ProofObligationList getProofObligations(POContextStack ctxt, Environment env); + abstract public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env); /** * Implemented by all multiple binds to allow visitor processing. diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleSeqBind.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleSeqBind.java index eded4aa79..c4709a94c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleSeqBind.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleSeqBind.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.po.patterns.visitors.POMultipleBindVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -48,9 +49,9 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return sequence.getProofObligations(ctxt, env); + return sequence.getProofObligations(ctxt, pogState, env); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleSetBind.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleSetBind.java index 92ad6832e..558a99a4b 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleSetBind.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleSetBind.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.po.patterns.visitors.POMultipleBindVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -48,9 +49,9 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return set.getProofObligations(ctxt, env); + return set.getProofObligations(ctxt, pogState, env); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleTypeBind.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleTypeBind.java index 845cb9f90..11abba6f1 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleTypeBind.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleTypeBind.java @@ -26,6 +26,7 @@ import com.fujitsu.vdmj.po.patterns.visitors.POMultipleBindVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.typechecker.Environment; @@ -48,7 +49,7 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { return new ProofObligationList(); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POSeqBind.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POSeqBind.java index e1c3bad48..ea82c081f 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POSeqBind.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POSeqBind.java @@ -30,6 +30,7 @@ import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.po.patterns.visitors.POBindVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -61,9 +62,9 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return sequence.getProofObligations(ctxt, env); + return sequence.getProofObligations(ctxt, pogState, env); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POSetBind.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POSetBind.java index f277ae733..d777966ee 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POSetBind.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POSetBind.java @@ -30,6 +30,7 @@ import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.po.patterns.visitors.POBindVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -61,9 +62,9 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return set.getProofObligations(ctxt, env); + return set.getProofObligations(ctxt, pogState, env); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POTypeBind.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POTypeBind.java index 57d0d2482..c6085baec 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POTypeBind.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POTypeBind.java @@ -29,6 +29,7 @@ import com.fujitsu.vdmj.po.patterns.visitors.POBindVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.typechecker.Environment; @@ -61,7 +62,7 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { return new ProofObligationList(); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/POBindStateFinder.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/POBindStateFinder.java new file mode 100644 index 000000000..b777b6fb2 --- /dev/null +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/POBindStateFinder.java @@ -0,0 +1,52 @@ +/******************************************************************************* + * + * Copyright (c) 2024 Nick Battle. + * + * Author: Nick Battle + * + * This file is part of VDMJ. + * + * VDMJ is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * VDMJ is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with VDMJ. If not, see . + * SPDX-License-Identifier: GPL-3.0-or-later + * + ******************************************************************************/ +package com.fujitsu.vdmj.po.patterns.visitors; + +import com.fujitsu.vdmj.po.POVisitorSet; +import com.fujitsu.vdmj.po.patterns.POBind; +import com.fujitsu.vdmj.tc.lex.TCNameSet; +import com.fujitsu.vdmj.tc.lex.TCNameToken; + +/** + * A visitor set to explore the PO tree and return the state names accessed. + */ +public class POBindStateFinder extends POLeafBindVisitor +{ + public POBindStateFinder(POVisitorSet visitors) + { + this.visitorSet = visitors; + } + + @Override + protected TCNameSet newCollection() + { + return new TCNameSet(); + } + + @Override + public TCNameSet caseBind(POBind node, Boolean arg) + { + return newCollection(); + } +} diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/POMultipleBindStateFinder.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/POMultipleBindStateFinder.java new file mode 100644 index 000000000..cd3041dca --- /dev/null +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/POMultipleBindStateFinder.java @@ -0,0 +1,52 @@ +/******************************************************************************* + * + * Copyright (c) 2024 Nick Battle. + * + * Author: Nick Battle + * + * This file is part of VDMJ. + * + * VDMJ is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * VDMJ is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with VDMJ. If not, see . + * SPDX-License-Identifier: GPL-3.0-or-later + * + ******************************************************************************/ +package com.fujitsu.vdmj.po.patterns.visitors; + +import com.fujitsu.vdmj.po.POVisitorSet; +import com.fujitsu.vdmj.po.patterns.POMultipleBind; +import com.fujitsu.vdmj.tc.lex.TCNameSet; +import com.fujitsu.vdmj.tc.lex.TCNameToken; + +/** + * A visitor set to explore the PO tree and return the state names accessed. + */ +public class POMultipleBindStateFinder extends POLeafMultipleBindVisitor +{ + public POMultipleBindStateFinder(POVisitorSet visitors) + { + this.visitorSet = visitors; + } + + @Override + protected TCNameSet newCollection() + { + return new TCNameSet(); + } + + @Override + public TCNameSet caseMultipleBind(POMultipleBind node, Boolean arg) + { + return newCollection(); + } +} diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAssignmentStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAssignmentStatement.java index f6d43966b..6dac5e905 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAssignmentStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAssignmentStatement.java @@ -28,12 +28,15 @@ import com.fujitsu.vdmj.po.definitions.POClassDefinition; import com.fujitsu.vdmj.po.definitions.POStateDefinition; import com.fujitsu.vdmj.po.expressions.POExpression; +import com.fujitsu.vdmj.po.statements.visitors.POStatementStateFinder; import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor; import com.fujitsu.vdmj.pog.POContextStack; import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.StateInvariantObligation; import com.fujitsu.vdmj.pog.SubTypeObligation; +import com.fujitsu.vdmj.tc.lex.TCNameSet; +import com.fujitsu.vdmj.tc.lex.TCNameToken; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.typechecker.Environment; import com.fujitsu.vdmj.typechecker.TypeComparator; @@ -83,9 +86,15 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog } obligations.addAll(target.getProofObligations(ctxt)); - obligations.addAll(exp.getProofObligations(ctxt, env)); + obligations.addAll(exp.getProofObligations(ctxt, pogState, env)); obligations.stateUpdate(pogState, exp); - pogState.didUpdateState(true); + + TCNameSet updates = this.apply(new POStatementStateFinder(), true); + + for (TCNameToken update: updates) + { + pogState.didUpdateState(update); + } if (!TypeComparator.isSubType(ctxt.checkType(exp, expType), targetType)) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POBlockStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POBlockStatement.java index c8c62745d..6eaab6b3c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POBlockStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POBlockStatement.java @@ -25,12 +25,13 @@ package com.fujitsu.vdmj.po.statements; import com.fujitsu.vdmj.lex.LexLocation; +import com.fujitsu.vdmj.po.definitions.POAssignmentDefinition; +import com.fujitsu.vdmj.po.definitions.PODefinition; import com.fujitsu.vdmj.po.definitions.PODefinitionList; import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.PODclContext; import com.fujitsu.vdmj.pog.POGState; -import com.fujitsu.vdmj.pog.POScopeContext; -import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -50,16 +51,19 @@ public POBlockStatement(LexLocation location, PODefinitionList assignmentDefs, P public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList obligations = assignmentDefs.getProofObligations(ctxt, pogState, env); - - ctxt.push(new POScopeContext()); - obligations.addAll(super.getProofObligations(ctxt, pogState, env)); - ctxt.pop(); - if (!assignmentDefs.isEmpty()) + POGState dclState = pogState.getLink(); + + for (PODefinition dcl: assignmentDefs) { - obligations.markUnchecked(ProofObligation.DCL_STATEMENT); + POAssignmentDefinition adef = (POAssignmentDefinition)dcl; + dclState.addDclState(adef.name); } + ctxt.push(new PODclContext(assignmentDefs)); + obligations.addAll(super.getProofObligations(ctxt, dclState, env)); + ctxt.pop(); + return obligations; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallObjectStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallObjectStatement.java index e0cad3b6e..248cd6787 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallObjectStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallObjectStatement.java @@ -72,12 +72,11 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog for (POExpression exp: args) { - obligations.addAll(exp.getProofObligations(ctxt, env)); + obligations.addAll(exp.getProofObligations(ctxt, pogState, env)); } // We have to assume the operation call accesses state - pogState.didReadState(true); - pogState.didUpdateState(true); + pogState.didUpdateState(); return obligations; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallStatement.java index 3f73e9970..91bf391e2 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallStatement.java @@ -60,12 +60,11 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog for (POExpression exp: args) { - obligations.addAll(exp.getProofObligations(ctxt, env)); + obligations.addAll(exp.getProofObligations(ctxt, pogState, env)); } // We have to assume the operation call accesses state - pogState.didReadState(true); - pogState.didUpdateState(true); + pogState.didUpdateState(); return obligations; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/PODefStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/PODefStatement.java index 7e919ee01..04d6653ce 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/PODefStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/PODefStatement.java @@ -56,7 +56,7 @@ public String toString() @Override public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList obligations = equalsDefs.getDefProofObligations(ctxt, env); + ProofObligationList obligations = equalsDefs.getDefProofObligations(ctxt, pogState, env); ctxt.push(new POLetDefContext(equalsDefs)); obligations.addAll(statement.getProofObligations(ctxt, pogState, env)); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POExitStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POExitStatement.java index 1d1b8a905..a50318293 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POExitStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POExitStatement.java @@ -56,7 +56,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog if (expression != null) { - obligations.addAll(expression.getProofObligations(ctxt, env)); + obligations.addAll(expression.getProofObligations(ctxt, pogState, env)); obligations.stateUpdate(pogState, expression); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForAllStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForAllStatement.java index 99a77f4bc..9fe2023a4 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForAllStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForAllStatement.java @@ -59,17 +59,13 @@ public String toString() @Override public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList obligations = set.getProofObligations(ctxt, env); + ProofObligationList obligations = set.getProofObligations(ctxt, pogState, env); obligations.stateUpdate(pogState, set); ProofObligationList loops = statement.getProofObligations(ctxt, pogState, env); - - if (statement.updatesState()) - { - loops.markUnchecked(ProofObligation.LOOP_STATEMENT); - } - + loops.markUnchecked(ProofObligation.LOOP_STATEMENT); obligations.addAll(loops); + return obligations; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForIndexStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForIndexStatement.java index f97947463..39a81535c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForIndexStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForIndexStatement.java @@ -65,24 +65,19 @@ public String toString() @Override public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList obligations = from.getProofObligations(ctxt, env); - obligations.addAll(to.getProofObligations(ctxt, env)); + ProofObligationList obligations = from.getProofObligations(ctxt, pogState, env); + obligations.addAll(to.getProofObligations(ctxt, pogState, env)); obligations.stateUpdate(pogState, from); if (by != null) { - obligations.addAll(by.getProofObligations(ctxt, env)); + obligations.addAll(by.getProofObligations(ctxt, pogState, env)); obligations.stateUpdate(pogState, by); } ctxt.push(new POScopeContext()); ProofObligationList loops = statement.getProofObligations(ctxt, pogState, env); - - if (statement.updatesState()) - { - loops.markUnchecked(ProofObligation.LOOP_STATEMENT); - } - + loops.markUnchecked(ProofObligation.LOOP_STATEMENT); obligations.addAll(loops); ctxt.pop(); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForPatternBindStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForPatternBindStatement.java index 47a8fb4a2..736dd5cf8 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForPatternBindStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForPatternBindStatement.java @@ -68,7 +68,7 @@ public String toString() @Override public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList list = exp.getProofObligations(ctxt, env); + ProofObligationList list = exp.getProofObligations(ctxt, pogState, env); list.stateUpdate(pogState, exp); if (patternBind.pattern != null) @@ -82,7 +82,7 @@ else if (patternBind.bind instanceof POTypeBind) else if (patternBind.bind instanceof POSetBind) { POSetBind bind = (POSetBind)patternBind.bind; - list.addAll(bind.set.getProofObligations(ctxt, env)); + list.addAll(bind.set.getProofObligations(ctxt, pogState, env)); ctxt.push(new POForAllSequenceContext(bind, exp)); list.add(new SetMemberObligation(bind.pattern.getMatchingExpression(), bind.set, ctxt)); @@ -91,7 +91,7 @@ else if (patternBind.bind instanceof POSetBind) else if (patternBind.bind instanceof POSeqBind) { POSeqBind bind = (POSeqBind)patternBind.bind; - list.addAll(bind.sequence.getProofObligations(ctxt, env)); + list.addAll(bind.sequence.getProofObligations(ctxt, pogState, env)); ctxt.push(new POForAllSequenceContext(bind, exp)); list.add(new SeqMemberObligation(bind.pattern.getMatchingExpression(), bind.sequence, ctxt)); @@ -99,13 +99,9 @@ else if (patternBind.bind instanceof POSeqBind) } ProofObligationList loops = statement.getProofObligations(ctxt, pogState, env); - - if (statement.updatesState()) - { - loops.markUnchecked(ProofObligation.LOOP_STATEMENT); - } - + loops.markUnchecked(ProofObligation.LOOP_STATEMENT); list.addAll(loops); + return list; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POIdentifierDesignator.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POIdentifierDesignator.java index a84c55f8a..dd6953227 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POIdentifierDesignator.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POIdentifierDesignator.java @@ -42,4 +42,10 @@ public String toString() { return name.getName(); } + + @Override + public String toPattern() throws IllegalArgumentException + { + return name.getName(); + } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POIfStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POIfStatement.java index 76eff7f92..f7d14e86a 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POIfStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POIfStatement.java @@ -78,7 +78,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog { POGStateList stateList = new POGStateList(); - ProofObligationList obligations = ifExp.getProofObligations(ctxt, env); + ProofObligationList obligations = ifExp.getProofObligations(ctxt, pogState, env); obligations.stateUpdate(pogState, ifExp); ctxt.push(new POImpliesContext(ifExp)); @@ -89,7 +89,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog for (POElseIfStatement stmt: elseList) { - ProofObligationList oblist = stmt.elseIfExp.getProofObligations(ctxt, env); + ProofObligationList oblist = stmt.elseIfExp.getProofObligations(ctxt, pogState, env); oblist.stateUpdate(pogState, stmt.elseIfExp); oblist.addAll(stmt.thenStmt.getProofObligations(ctxt, stateList.addCopy(pogState), env)); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POLetBeStStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POLetBeStStatement.java index a15aa0343..03c49c712 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POLetBeStStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POLetBeStStatement.java @@ -64,12 +64,12 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog { ProofObligationList obligations = new ProofObligationList(); obligations.add(new LetBeExistsObligation(this, ctxt)); - obligations.addAll(bind.getProofObligations(ctxt, env)); + obligations.addAll(bind.getProofObligations(ctxt, pogState, env)); if (suchThat != null) { ctxt.push(new POForAllContext(this)); - ProofObligationList oblist = suchThat.getProofObligations(ctxt, env); + ProofObligationList oblist = suchThat.getProofObligations(ctxt, pogState, env); oblist.stateUpdate(pogState, suchThat); obligations.addAll(oblist); ctxt.pop(); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POLetDefStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POLetDefStatement.java index f0df04d3b..dbf34ae7d 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POLetDefStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POLetDefStatement.java @@ -55,7 +55,7 @@ public String toString() @Override public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList obligations = localDefs.getDefProofObligations(ctxt, env); + ProofObligationList obligations = localDefs.getDefProofObligations(ctxt, pogState, env); ctxt.push(new POLetDefContext(this.localDefs)); obligations.addAll(statement.getProofObligations(ctxt, pogState, env)); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POReturnStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POReturnStatement.java index 2a99e69bb..90510f5b2 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POReturnStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POReturnStatement.java @@ -56,8 +56,9 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog if (expression != null) { - obligations.addAll(expression.getProofObligations(ctxt, env)); - obligations.stateUpdate(pogState, expression); + // Don't process POG state here, because we're returning, so the expression can + // have no further effect in the operation. + obligations.addAll(expression.getProofObligations(ctxt, new POGState(), env)); } return obligations; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POSpecificationStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POSpecificationStatement.java index bfd8344e3..811ec2065 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POSpecificationStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POSpecificationStatement.java @@ -71,19 +71,19 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog { for (POErrorCase err: errors) { - obligations.addAll(err.left.getProofObligations(ctxt, env)); - obligations.addAll(err.right.getProofObligations(ctxt, env)); + obligations.addAll(err.left.getProofObligations(ctxt, pogState, env)); + obligations.addAll(err.right.getProofObligations(ctxt, pogState, env)); } } if (precondition != null) { - obligations.addAll(precondition.getProofObligations(ctxt, env)); + obligations.addAll(precondition.getProofObligations(ctxt, pogState, env)); } if (postcondition != null) { - obligations.addAll(postcondition.getProofObligations(ctxt, env)); + obligations.addAll(postcondition.getProofObligations(ctxt, pogState, env)); } return obligations; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POStartStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POStartStatement.java index 72dfbe97d..41d49ebf6 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POStartStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POStartStatement.java @@ -46,7 +46,7 @@ public POStartStatement(LexLocation location, POExpression obj) @Override public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return objects.getProofObligations(ctxt, env); + return objects.getProofObligations(ctxt, pogState, env); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POStateDesignator.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POStateDesignator.java index c269f69c9..0d83d3719 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POStateDesignator.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POStateDesignator.java @@ -45,6 +45,15 @@ public POStateDesignator(LexLocation location) @Override abstract public String toString(); + + /** + * A pattern, such that "let = in ..." can be used in POs. This + * is not always possible. + */ + public String toPattern() throws IllegalArgumentException + { + throw new IllegalArgumentException("Cannot generate pattern for " + this); + } /** * @param ctxt diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POStopStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POStopStatement.java index bd51eb82a..166529741 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POStopStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POStopStatement.java @@ -46,7 +46,7 @@ public POStopStatement(LexLocation location, POExpression obj) @Override public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return objects.getProofObligations(ctxt, env); + return objects.getProofObligations(ctxt, pogState, env); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POTixeStmtAlternative.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POTixeStmtAlternative.java index 1298ae708..5d8452ff2 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POTixeStmtAlternative.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POTixeStmtAlternative.java @@ -68,14 +68,14 @@ else if (patternBind.bind instanceof POTypeBind) else if (patternBind.bind instanceof POSetBind) { POSetBind bind = (POSetBind)patternBind.bind; - list.addAll(bind.set.getProofObligations(ctxt, env)); + list.addAll(bind.set.getProofObligations(ctxt, pogState, env)); list.add(new SetMemberObligation(bind.pattern.getMatchingExpression(), bind.set, ctxt)); } else if (patternBind.bind instanceof POSeqBind) { POSeqBind bind = (POSeqBind)patternBind.bind; - list.addAll(bind.sequence.getProofObligations(ctxt, env)); + list.addAll(bind.sequence.getProofObligations(ctxt, pogState, env)); list.add(new SeqMemberObligation(bind.pattern.getMatchingExpression(), bind.sequence, ctxt)); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POTrapStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POTrapStatement.java index 503da5e7f..83595e303 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POTrapStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POTrapStatement.java @@ -75,14 +75,14 @@ else if (patternBind.bind instanceof POTypeBind) else if (patternBind.bind instanceof POSetBind) { POSetBind bind = (POSetBind)patternBind.bind; - list.addAll(bind.set.getProofObligations(ctxt, env)); + list.addAll(bind.set.getProofObligations(ctxt, pogState, env)); list.add(new SetMemberObligation(bind.pattern.getMatchingExpression(), bind.set, ctxt)); } else if (patternBind.bind instanceof POSeqBind) { POSeqBind bind = (POSeqBind)patternBind.bind; - list.addAll(bind.sequence.getProofObligations(ctxt, env)); + list.addAll(bind.sequence.getProofObligations(ctxt, pogState, env)); list.add(new SeqMemberObligation(bind.pattern.getMatchingExpression(), bind.sequence, ctxt)); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POWhileStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POWhileStatement.java index acd4f568b..a0cbabb42 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POWhileStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POWhileStatement.java @@ -59,7 +59,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog ProofObligationList obligations = new ProofObligationList(); obligations.add(new WhileLoopObligation(this, ctxt)); - obligations.addAll(exp.getProofObligations(ctxt, env)); + obligations.addAll(exp.getProofObligations(ctxt, pogState, env)); obligations.stateUpdate(pogState, exp); ProofObligationList loops = statement.getProofObligations(ctxt, pogState, env); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/visitors/POStatementStateFinder.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/visitors/POStatementStateFinder.java index 952e33022..7adef8a01 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/visitors/POStatementStateFinder.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/visitors/POStatementStateFinder.java @@ -24,16 +24,22 @@ package com.fujitsu.vdmj.po.statements.visitors; +import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.POVisitorSet; import com.fujitsu.vdmj.po.definitions.PODefinition; import com.fujitsu.vdmj.po.definitions.POValueDefinition; import com.fujitsu.vdmj.po.definitions.visitors.PODefinitionStateFinder; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionStateFinder; +import com.fujitsu.vdmj.po.patterns.visitors.POBindStateFinder; +import com.fujitsu.vdmj.po.patterns.visitors.POMultipleBindStateFinder; import com.fujitsu.vdmj.po.statements.POAssignmentStatement; import com.fujitsu.vdmj.po.statements.POCallObjectStatement; import com.fujitsu.vdmj.po.statements.POCallStatement; +import com.fujitsu.vdmj.po.statements.POFieldDesignator; import com.fujitsu.vdmj.po.statements.POIdentifierDesignator; import com.fujitsu.vdmj.po.statements.POLetDefStatement; +import com.fujitsu.vdmj.po.statements.POMapSeqDesignator; +import com.fujitsu.vdmj.po.statements.POStateDesignator; import com.fujitsu.vdmj.po.statements.POStatement; import com.fujitsu.vdmj.tc.lex.TCNameSet; import com.fujitsu.vdmj.tc.lex.TCNameToken; @@ -44,6 +50,8 @@ */ public class POStatementStateFinder extends POLeafStatementVisitor { + private static TCNameToken EVERYTHING = new TCNameToken(LexLocation.ANY, "*", "*"); + public POStatementStateFinder() { super(false); @@ -53,12 +61,11 @@ public POStatementStateFinder() @Override protected void setVisitors() { + statementVisitor = POStatementStateFinder.this; definitionVisitor = new PODefinitionStateFinder(this); expressionVisitor = new POExpressionStateFinder(this); - statementVisitor = POStatementStateFinder.this; - patternVisitor = null; - bindVisitor = null; - multiBindVisitor = null; + bindVisitor = new POBindStateFinder(this); + multiBindVisitor = new POMultipleBindStateFinder(this); } @Override @@ -72,30 +79,21 @@ protected TCNameSet newCollection() @Override public TCNameSet caseAssignmentStatement(POAssignmentStatement node, Boolean updates) { - TCNameSet all = newCollection(); - if (updates) { - if (node.target instanceof POIdentifierDesignator) - { - POIdentifierDesignator id = (POIdentifierDesignator)node.target; - all.add(id.name); - } - else - { - // Updates something... - all.add(new TCNameToken(node.location, "?", node.target.toString())); - } + return designatorUpdates(node.target); + } + else + { + return designatorReads(node.target); } - - return all; } @Override public TCNameSet caseCallStatement(POCallStatement node, Boolean updates) { TCNameSet all = newCollection(); - all.add(new TCNameToken(node.location, "?", "?")); // Not state, but assumed to access state. + all.add(EVERYTHING); // Not state, but assumed to access state. return all; } @@ -103,7 +101,7 @@ public TCNameSet caseCallStatement(POCallStatement node, Boolean updates) public TCNameSet caseCallObjectStatement(POCallObjectStatement node, Boolean updates) { TCNameSet all = newCollection(); - all.add(new TCNameToken(node.location, "?", "?")); // Not state, but assumed to access state. + all.add(EVERYTHING); // Not state, but assumed to access state. return all; } @@ -142,4 +140,55 @@ public TCNameSet caseStatement(POStatement node, Boolean updates) { return newCollection(); } + + /** + * Identify the state names that are updated by a given state designator. + */ + private TCNameSet designatorUpdates(POStateDesignator sd) + { + TCNameSet all = newCollection(); + + if (sd instanceof POIdentifierDesignator) + { + POIdentifierDesignator id = (POIdentifierDesignator)sd; + all.add(id.name); + } + else if (sd instanceof POFieldDesignator) + { + POFieldDesignator fd = (POFieldDesignator)sd; + all.addAll(designatorUpdates(fd.object)); + } + else if (sd instanceof POMapSeqDesignator) + { + POMapSeqDesignator msd = (POMapSeqDesignator)sd; + all.addAll(designatorUpdates(msd.mapseq)); + } + + return all; + } + + /** + * Identify the names that are read by a given state designator. + */ + private TCNameSet designatorReads(POStateDesignator sd) + { + if (sd instanceof POIdentifierDesignator) + { + return newCollection(); + } + else if (sd instanceof POFieldDesignator) + { + POFieldDesignator fd = (POFieldDesignator)sd; + return designatorReads(fd.object); + } + else if (sd instanceof POMapSeqDesignator) + { + POMapSeqDesignator msd = (POMapSeqDesignator)sd; + TCNameSet all = designatorReads(msd.mapseq); + all.addAll(visitorSet.applyExpressionVisitor(msd.exp, false)); + return all; + } + + return newCollection(); + } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/PODclContext.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/PODclContext.java new file mode 100644 index 000000000..9dd156146 --- /dev/null +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/PODclContext.java @@ -0,0 +1,71 @@ +/******************************************************************************* + * + * Copyright (c) 2016 Fujitsu Services Ltd. + * + * Author: Nick Battle + * + * This file is part of VDMJ. + * + * VDMJ is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * VDMJ is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with VDMJ. If not, see . + * SPDX-License-Identifier: GPL-3.0-or-later + * + ******************************************************************************/ + +package com.fujitsu.vdmj.pog; + +import com.fujitsu.vdmj.po.definitions.POAssignmentDefinition; +import com.fujitsu.vdmj.po.definitions.PODefinition; +import com.fujitsu.vdmj.po.definitions.PODefinitionList; + +public class PODclContext extends POContext +{ + public final PODefinitionList assignmentDefs; + + public PODclContext(PODefinitionList assignmentDefs) + { + this.assignmentDefs = assignmentDefs; + } + + @Override + public boolean isScopeBoundary() + { + return true; + } + + @Override + public String getSource() + { + StringBuilder sb = new StringBuilder(); + + if (!assignmentDefs.isEmpty()) + { + sb.append("let "); + String sep = ""; + + for (PODefinition def: assignmentDefs) + { + sb.append(sep); + POAssignmentDefinition adef = (POAssignmentDefinition)def; + sb.append(adef.name); + sb.append(" = "); + sb.append(adef.expression); + sep = ", "; + } + + sb.append(" in"); + } + + return sb.toString(); + } +} diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POGState.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POGState.java index 26529f422..adc89f5c7 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POGState.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POGState.java @@ -23,6 +23,10 @@ ******************************************************************************/ package com.fujitsu.vdmj.pog; +import com.fujitsu.vdmj.tc.lex.TCNameList; +import com.fujitsu.vdmj.tc.lex.TCNameToken; +import com.fujitsu.vdmj.util.Utils; + /** * A class to hold state information for POG of statements, which involve potentially * changing state variables. @@ -30,49 +34,80 @@ public class POGState { private boolean hasUpdatedState; - private boolean hasReadState; + private POGState outerState; + private TCNameList locals; public POGState() { hasUpdatedState = false; - hasReadState = false; + outerState = null; + locals = new TCNameList(); } - private POGState(boolean hasUpdatedState, boolean hasReadState) + private POGState(boolean hasUpdatedState, POGState outerState) { this.hasUpdatedState = hasUpdatedState; - this.hasReadState = hasReadState; + this.outerState = outerState; + this.locals = new TCNameList(); } @Override public String toString() { - return (hasUpdatedState ? "has" : "has not") + " updated state; " + - (hasReadState ? "has" : "has not") + " read state"; + return (hasUpdatedState ? "has" : "has not") + " updated state" + + (locals.isEmpty() ? "" : Utils.listToString("(locals ", locals, ", ", ")")); } public POGState getCopy() { - return new POGState(hasUpdatedState, hasReadState); + return new POGState(hasUpdatedState, outerState); + } + + public POGState getLink() + { + return new POGState(false, this); } public boolean hasUpdatedState() { - return hasUpdatedState; + return hasUpdatedState || (outerState != null && outerState.hasUpdatedState()); + } + + public void setUpdateState(boolean updatedState) + { + hasUpdatedState = hasUpdatedState || updatedState; } - public boolean hasReadState() + public void didUpdateState() // Used by call statements { - return hasReadState; + if (outerState != null) + { + outerState.didUpdateState(); + } + else + { + hasUpdatedState = true; // Module level + } } - public void didUpdateState(boolean flag) + public void didUpdateState(TCNameToken name) { - hasUpdatedState = hasUpdatedState || flag; + if (locals.contains(name)) + { + hasUpdatedState = true; // A local dcl update + } + else if (outerState != null) + { + outerState.didUpdateState(name); // May be an outer* local + } + else + { + hasUpdatedState = true; // A module state update + } } - public void didReadState(boolean flag) + public void addDclState(TCNameToken name) { - hasReadState = hasReadState || flag; + locals.add(name); } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POGStateList.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POGStateList.java index c036d20e3..31683bd92 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POGStateList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POGStateList.java @@ -49,15 +49,12 @@ public POGState addCopy(POGState parent) public void combineInto(POGState parent) { boolean hasUpdatedState = false; - boolean hasReadState = false; for (POGState state: this) { hasUpdatedState = hasUpdatedState || state.hasUpdatedState(); - hasReadState = hasReadState || state.hasReadState(); } - parent.didUpdateState(hasUpdatedState); - parent.didReadState(hasReadState); + parent.setUpdateState(hasUpdatedState); } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java index 7f93b7c0c..b80855701 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java @@ -59,8 +59,8 @@ abstract public class ProofObligation implements Comparable public static final String REQUIRES_VDM10 = "Obligation requires VDM10"; public static final String BODY_UPDATES_STATE = "Operation body updates state"; public static final String LOOP_STATEMENT = "Loop modifies state"; - public static final String DCL_STATEMENT = "Block contains dcl assignments"; public static final String HAS_UPDATED_STATE = "Previous statements updated state"; + public static final String COMPLEX_ASSIGNMENT = "Assignment too complex"; public final LexLocation location; public final POType kind; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java index 92d583b26..0365de1d7 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java @@ -200,7 +200,7 @@ private void typeCheck(ProofObligation obligation, String mname, Environment env if (!end.is(Token.EOF)) { - throw new ParserException(2330, "Tokens found after expression at " + end, LexLocation.ANY, 0); + throw new ParserException(2330, "POG: Tokens found after obligation at " + end, LexLocation.ANY, 0); } TCExpression tcexp = ClassMapper.getInstance(TCNode.MAPPINGS).convertLocal(ast); @@ -210,7 +210,7 @@ private void typeCheck(ProofObligation obligation, String mname, Environment env if (!potype.isType(TCBooleanType.class, obligation.location)) { - throw new ParserException(2330, "PO is not boolean?", obligation.location, 0); + throw new ParserException(2336, "POG: Obligation is not boolean?", obligation.location, 0); } // Weed out errors that we can cope with @@ -245,7 +245,7 @@ private void typeCheck(ProofObligation obligation, String mname, Environment env if (TypeChecker.getErrorCount() > 0) { - throw new ParserException(2330, "PO has type errors?", obligation.location, 0); + throw new ParserException(2337, "POG Obligation has type errors?", obligation.location, 0); } obligation.setCheckedExpression(tcexp); @@ -256,7 +256,7 @@ private void typeCheck(ProofObligation obligation, String mname, Environment env POExpression poexp = ClassMapper.getInstance(PONode.MAPPINGS).convertLocal(tcexp); POContextStack stack = new POContextStack(); stack.push(new PONameContext()); // Must have one context - ProofObligationList popos = poexp.getProofObligations(stack, env); + ProofObligationList popos = poexp.getProofObligations(stack, new POGState(), env); obligation.setHasObligations(!popos.isEmpty()); } @@ -275,18 +275,17 @@ public ProofObligationList markUnchecked(String message) } /** - * Update the obligations in this list because of the current POGState, and then update - * the POGState to account for the state read/updates in expression. + * Update the obligations in this list because of the current POGState and the state read + * by the expression. This is used by various statements and definitions, to suppress + * obligations that cannot yet be checked. */ public void stateUpdate(POGState pstate, POExpression expression) { boolean readsState = expression.readsState(); - if (pstate.hasUpdatedState() && readsState) + if (readsState && pstate.hasUpdatedState()) { markUnchecked(ProofObligation.HAS_UPDATED_STATE); } - - pstate.didReadState(readsState); } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInvariantObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInvariantObligation.java index 3ad626911..558dd349c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInvariantObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInvariantObligation.java @@ -40,8 +40,15 @@ public StateInvariantObligation(POAssignmentStatement ass, POContextStack ctxt) super(ass.location, POType.STATE_INVARIANT, ctxt); StringBuilder sb = new StringBuilder(); - // Note a StateDesignator is not a pattern, so this may not work! - sb.append("let " + ass.target + " = " + ass.exp + " in\n"); + try + { + sb.append("let " + ass.target.toPattern() + " = " + ass.exp + " in\n"); + } + catch (IllegalArgumentException e) + { + // Can't represent designator as a pattern, so cannot check PO + markUnchecked(ProofObligation.COMPLEX_ASSIGNMENT); + } if (ass.classDefinition != null) { @@ -54,8 +61,8 @@ public StateInvariantObligation(POAssignmentStatement ass, POContextStack ctxt) sb.append("let "); sb.append(def.invPattern); sb.append(" = "); - sb.append(def.name); - sb.append(" in "); + sb.append(def.toPattern()); + sb.append(" in\n"); sb.append(def.invExpression); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/typechecker/ModuleTypeChecker.java b/vdmj/src/main/java/com/fujitsu/vdmj/typechecker/ModuleTypeChecker.java index b83d49fb9..6b3489f4b 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/typechecker/ModuleTypeChecker.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/typechecker/ModuleTypeChecker.java @@ -233,6 +233,23 @@ public void typeCheck() m.annotations.tcAfter(m, e); } } + + // After the VALUES pass, ValueDefinitions will have replaced their TCUntypedDefinition "defs" + // with typed TCLocalDefinitions, so we refresh the export/importDefs to allow later passes + // to see the correct types of imported definitions. + + if (pass == Pass.VALUES) + { + for (TCModule m: modules) + { + m.processExports(); // Re-populate exports + } + + for (TCModule m: modules) + { + m.processImports(modules); // Re-populate importDefs + } + } } // Prepare to look for recursive loops @@ -243,12 +260,12 @@ public void typeCheck() for (TCModule m: modules) { - m.processExports(); // Re-populate exports + m.processExports(); // Re-populate exports again } for (TCModule m: modules) { - m.processImports(modules); // Re-populate importDefs + m.processImports(modules); // Re-populate importDefs again try { diff --git a/vdmj/src/test/java/com/fujitsu/vdmj/junit/PogTest.java b/vdmj/src/test/java/com/fujitsu/vdmj/junit/PogTest.java index c5e3426ea..ebaaa92db 100644 --- a/vdmj/src/test/java/com/fujitsu/vdmj/junit/PogTest.java +++ b/vdmj/src/test/java/com/fujitsu/vdmj/junit/PogTest.java @@ -147,8 +147,8 @@ protected void tearDown() throws Exception /* 81 */ "(forall i:int, obj_A(iv |-> iv):A &\n (1 = i => \n ((m(1) < 10) =>\n 1 in set dom m)))\n", /* 82 */ "(forall i:int, obj_A(iv |-> iv):A &\n (1 = i => \n (not (m(1) < 10) =>\n 2 in set dom m)))\n", /* 83 */ "(forall i:int, obj_A(iv |-> iv):A &\n (not 1 = i =>\n (2 = i => \n 3 in set dom m)))\n", - /* 84 */ "(forall obj_A(iv |-> iv):A &\n while (x > 0) do ...)\n", - /* 85 */ "(forall obj_A(iv |-> iv):A &\n let iv = (iv + 1) in (iv < 10))\n", + /* 84 */ "(forall obj_A(iv |-> iv):A &\n (let x = 10 in\n while (x > 0) do ...))\n", + /* 85 */ "(forall obj_A(iv |-> iv):A &\n (let x = 10 in\n let iv = (iv + 1) in (iv < 10)))\n", }; public void testPOG() throws Exception