diff --git a/quickcheck/src/main/java/quickcheck/QuickCheck.java b/quickcheck/src/main/java/quickcheck/QuickCheck.java index 91fa512cf..996748104 100644 --- a/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -408,7 +408,8 @@ public void checkObligation(ProofObligation po, StrategyResults sresults) if (!po.isCheckable) { - infof(POStatus.UNCHECKED, "PO #%d, UNCHECKED\n", po.number); + infof(POStatus.UNCHECKED, "PO #%d, UNCHECKED %s\n", + po.number, (po.message == null ? "" : "(" + po.message + ")")); return; } else if (sresults.provedBy != null) diff --git a/quickcheck/src/main/java/quickcheck/visitors/FixedRangeCreator.java b/quickcheck/src/main/java/quickcheck/visitors/FixedRangeCreator.java index 48df99a0e..b008147b8 100644 --- a/quickcheck/src/main/java/quickcheck/visitors/FixedRangeCreator.java +++ b/quickcheck/src/main/java/quickcheck/visitors/FixedRangeCreator.java @@ -193,7 +193,7 @@ public ValueSet caseNaturalOneType(TCNaturalOneType node, Integer limit) { try { - result.addNoSort(new NaturalOneValue(a)); + result.addSorted(new NaturalOneValue(a)); } catch (Exception e) { @@ -213,7 +213,7 @@ public ValueSet caseNaturalType(TCNaturalType node, Integer limit) { try { - result.addNoSort(new NaturalValue(a)); + result.addSorted(new NaturalValue(a)); } catch (Exception e) { @@ -235,11 +235,11 @@ public ValueSet caseIntegerType(TCIntegerType node, Integer limit) case 1: return new ValueSet(new IntegerValue(0)); default: int a = -limit/2; - result.addNoSort(new IntegerValue(a++)); + result.addSorted(new IntegerValue(a++)); while (result.size() < limit) { - result.addNoSort(new IntegerValue(a)); + result.addSorted(new IntegerValue(a)); a++; } diff --git a/quickcheck/src/main/java/quickcheck/visitors/RangeCreator.java b/quickcheck/src/main/java/quickcheck/visitors/RangeCreator.java index c0e6330a4..47bda4dcb 100644 --- a/quickcheck/src/main/java/quickcheck/visitors/RangeCreator.java +++ b/quickcheck/src/main/java/quickcheck/visitors/RangeCreator.java @@ -115,26 +115,37 @@ protected List powerLimit(ValueSet source, int limit, boolean incEmpty /** * Return the lowest integer power of n that is <= limit. If n < 2, - * just return 1. + * just return limit. + * + * Used to calculate how many field values to generate for an n-field object. + * For example, a three field tuple/record with one value each gives 1x1x1=1 records; + * with two values each it gives 2x2x2=8 values, with three 3x3x3=27 values. So to + * generate up to N values from F field combinations, we need to find the largest n, + * such that n^F < N. + * + * If there is only one field, we can generate N values. */ - protected int leastPower(int n, int limit) + protected int leastPower(int F, int N) { - int power = 1; - - if (n > 1) + if (F > 1) { - int value = n; + int power = 1; + int value = F; - while (value < limit) + while (value < N) { - value = value * n; + value = value * F; power++; } + + return power - 1; + } + else + { + return N; } - - return power; } - + /** * Attempt to produce a function that matches a (possibly polymorphic) TCFunctionType. */ diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INIndicesExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INIndicesExpression.java index 507c74a1b..6264e0478 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INIndicesExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INIndicesExpression.java @@ -61,10 +61,10 @@ public Value eval(Context ctxt) for (int i=1; i<= seq.size(); i++) { - result.addNoCheck(new NaturalOneValue(i)); + result.addSorted(new NaturalOneValue(i)); } - return new SetValue(result); + return new SetValue(result, false); } catch (ValueException e) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INPowerSetExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INPowerSetExpression.java index 00e7bfc0b..3d7d4532a 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INPowerSetExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INPowerSetExpression.java @@ -65,7 +65,7 @@ public Value eval(Context ctxt) for (ValueSet v: psets) { - rs.addNoCheck(new SetValue(v)); + rs.addSorted(new SetValue(v, false)); // Already sorted } // The additions above can take a while, because all of the SetValues are diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INSetRangeExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INSetRangeExpression.java index 3f519b08f..e488e2feb 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INSetRangeExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INSetRangeExpression.java @@ -67,7 +67,7 @@ public Value eval(Context ctxt) while (from.compareTo(to) <= 0) { - set.addNoCheck(new IntegerValue(from)); + set.addSorted(new IntegerValue(from)); from = from.add(BigInteger.ONE); } 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 c1a878ecd..d06f98790 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 @@ -73,8 +73,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment if (!TypeComparator.isSubType(ctxt.checkType(expression, expType), type)) { - obligations.add( - new SubTypeObligation(expression, type, expType, ctxt)); + obligations.add(new SubTypeObligation(expression, type, expType, ctxt)); } return obligations; 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 c99e887ff..32bf182df 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,7 +27,6 @@ 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.PONoCheckContext; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.StateInvariantObligation; import com.fujitsu.vdmj.tc.lex.TCNameToken; @@ -69,9 +68,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment if (!classDefinition.hasConstructors) { - ctxt.push(new PONoCheckContext()); list.add(new StateInvariantObligation(this, ctxt)); - ctxt.pop(); } return list; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitOperationDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitOperationDefinition.java index 5030f0834..707f01fec 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitOperationDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitOperationDefinition.java @@ -35,14 +35,15 @@ import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.po.patterns.POPattern; import com.fujitsu.vdmj.po.patterns.POPatternList; +import com.fujitsu.vdmj.po.statements.POSimpleBlockStatement; import com.fujitsu.vdmj.po.statements.POStatement; import com.fujitsu.vdmj.pog.OperationPostConditionObligation; import com.fujitsu.vdmj.pog.POContextStack; import com.fujitsu.vdmj.pog.POFunctionDefinitionContext; import com.fujitsu.vdmj.pog.POImpliesContext; -import com.fujitsu.vdmj.pog.PONoCheckContext; import com.fujitsu.vdmj.pog.POOperationDefinitionContext; import com.fujitsu.vdmj.pog.ParameterPatternObligation; +import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.StateInvariantObligation; import com.fujitsu.vdmj.pog.SubTypeObligation; @@ -159,83 +160,71 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment obligations.addAll(postdef.getProofObligations(ctxt, env)); } - ctxt.push(new PONoCheckContext()); obligations.add(new OperationPostConditionObligation(this, ctxt)); - ctxt.pop(); } - boolean updatesState = body.updatesState(); + boolean updatesState = !(body instanceof POSimpleBlockStatement) && body.updatesState(); if (stateDefinition != null) { - if (!updatesState) + ctxt.push(new POOperationDefinitionContext(this, (precondition != null), stateDefinition, true)); + ProofObligationList oblist = body.getProofObligations(ctxt, null, env); + ctxt.pop(); + + if (updatesState) { - ctxt.push(new POOperationDefinitionContext(this, (precondition != null), stateDefinition, true)); - obligations.addAll(body.getProofObligations(ctxt, null, env)); - ctxt.pop(); - } - else - { - ctxt.push(new PONoCheckContext()); - ctxt.push(new POOperationDefinitionContext(this, (precondition != null), stateDefinition, true)); - obligations.addAll(body.getProofObligations(ctxt, null, env)); - ctxt.pop(); - ctxt.pop(); + oblist.markUnchecked(ProofObligation.BODY_UPDATES_STATE); } + + obligations.addAll(oblist); } else if (classDefinition != null) { - if (Settings.release == Release.VDM_10) // Uses the obj_C pattern + ctxt.push(new POOperationDefinitionContext(this, (precondition != null), classDefinition, true)); + ProofObligationList oblist = body.getProofObligations(ctxt, null, env); + ctxt.pop(); + + if (Settings.release != Release.VDM_10) // Uses the obj_C pattern in OperationDefContext + { + oblist.markUnchecked(ProofObligation.REQUIRES_VDM10); + } + else if (precondition != null) // pre_op undefined in VDM++ { - if (precondition == null && !updatesState) - { - ctxt.push(new POOperationDefinitionContext(this, false, classDefinition, true)); - obligations.addAll(body.getProofObligations(ctxt, null, env)); - ctxt.pop(); - } - else // Can't check "pre_op(args, new X(args)) => ..." - { - ctxt.push(new PONoCheckContext()); - ctxt.push(new POOperationDefinitionContext(this, true, classDefinition, true)); - obligations.addAll(body.getProofObligations(ctxt, null, env)); - ctxt.pop(); - ctxt.pop(); - } + oblist.markUnchecked(ProofObligation.UNCHECKED_VDMPP); } + else if (updatesState) + { + oblist.markUnchecked(ProofObligation.BODY_UPDATES_STATE); + } + + obligations.addAll(oblist); } else // Flat spec with no state defined { - if (!updatesState) - { - ctxt.push(new POOperationDefinitionContext(this, (precondition != null), null, true)); - obligations.addAll(body.getProofObligations(ctxt, null, env)); - ctxt.pop(); - } - else + ctxt.push(new POOperationDefinitionContext(this, (precondition != null), null, true)); + ProofObligationList oblist = body.getProofObligations(ctxt, null, env); + ctxt.pop(); + + if (updatesState) { - ctxt.push(new PONoCheckContext()); - ctxt.push(new POOperationDefinitionContext(this, (precondition != null), null, true)); - obligations.addAll(body.getProofObligations(ctxt, null, env)); - ctxt.pop(); - ctxt.pop(); + oblist.markUnchecked(ProofObligation.BODY_UPDATES_STATE); } + + obligations.addAll(oblist); } if (isConstructor && classDefinition != null && classDefinition.invariant != null) { - ctxt.push(new PONoCheckContext()); obligations.add(new StateInvariantObligation(this, ctxt)); - ctxt.pop(); } if (!isConstructor && !TypeComparator.isSubType(actualResult, type.result)) { - ctxt.push(new PONoCheckContext()); - obligations.add(new SubTypeObligation(this, actualResult, ctxt)); - ctxt.pop(); + obligations.add(new SubTypeObligation(this, actualResult, ctxt). + markUnchecked(ProofObligation.NOT_YET_SUPPORTED)); } if (annotations != null) annotations.poAfter(this, obligations, ctxt); 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 5b14eaa99..e191a7f86 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 @@ -37,6 +37,7 @@ import com.fujitsu.vdmj.po.patterns.POPatternList; import com.fujitsu.vdmj.po.statements.POErrorCaseList; import com.fujitsu.vdmj.po.statements.POExternalClauseList; +import com.fujitsu.vdmj.po.statements.POSimpleBlockStatement; import com.fujitsu.vdmj.po.statements.POStatement; import com.fujitsu.vdmj.po.types.POPatternListTypePair; import com.fujitsu.vdmj.po.types.POPatternListTypePairList; @@ -45,9 +46,9 @@ import com.fujitsu.vdmj.pog.POContextStack; import com.fujitsu.vdmj.pog.POFunctionDefinitionContext; import com.fujitsu.vdmj.pog.POImpliesContext; -import com.fujitsu.vdmj.pog.PONoCheckContext; import com.fujitsu.vdmj.pog.POOperationDefinitionContext; import com.fujitsu.vdmj.pog.ParameterPatternObligation; +import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.SatisfiabilityObligation; import com.fujitsu.vdmj.pog.StateInvariantObligation; @@ -79,7 +80,7 @@ public class POImplicitOperationDefinition extends PODefinition public final POExplicitFunctionDefinition predef; public final POExplicitFunctionDefinition postdef; public final TCType actualResult; - public final PODefinition state; + public final PODefinition stateDefinition; public final boolean isConstructor; public POImplicitOperationDefinition(POAnnotationList annotations, @@ -111,7 +112,7 @@ public POImplicitOperationDefinition(POAnnotationList annotations, this.predef = predef; this.postdef = postdef; this.actualResult = actualResult; - this.state = stateDefinition; + this.stateDefinition = stateDefinition; this.isConstructor = isConstructor; } @@ -184,39 +185,73 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment obligations.addAll(postdef.getProofObligations(ctxt, env)); } - ctxt.push(new PONoCheckContext()); obligations.add(new OperationPostConditionObligation(this, ctxt)); - ctxt.pop(); } if (body != null) { - if (body.updatesState()) + boolean updatesState = !(body instanceof POSimpleBlockStatement) && body.updatesState(); + + if (stateDefinition != null) { - ctxt.push(new PONoCheckContext()); - obligations.addAll(body.getProofObligations(ctxt, null, env)); + ctxt.push(new POOperationDefinitionContext(this, (precondition != null), stateDefinition, true)); + ProofObligationList oblist = body.getProofObligations(ctxt, null, env); ctxt.pop(); + + if (updatesState) + { + oblist.markUnchecked(ProofObligation.BODY_UPDATES_STATE); + } + + obligations.addAll(oblist); } - else + else if (classDefinition != null) + { + ctxt.push(new POOperationDefinitionContext(this, (precondition != null), classDefinition, true)); + ProofObligationList oblist = body.getProofObligations(ctxt, null, env); + ctxt.pop(); + + if (Settings.release != Release.VDM_10) // Uses the obj_C pattern in OperationDefContext + { + oblist.markUnchecked(ProofObligation.REQUIRES_VDM10); + } + else if (precondition != null) // pre_op undefined in VDM++ + { + oblist.markUnchecked(ProofObligation.UNCHECKED_VDMPP); + } + else if (updatesState) + { + oblist.markUnchecked(ProofObligation.BODY_UPDATES_STATE); + } + + obligations.addAll(oblist); + } + else // Flat spec with no state defined { - obligations.addAll(body.getProofObligations(ctxt, null, env)); + ctxt.push(new POOperationDefinitionContext(this, (precondition != null), null, true)); + ProofObligationList oblist = body.getProofObligations(ctxt, null, env); + ctxt.pop(); + + if (updatesState) + { + oblist.markUnchecked(ProofObligation.BODY_UPDATES_STATE); + } + + obligations.addAll(oblist); } if (isConstructor && classDefinition != null && classDefinition.invariant != null) { - ctxt.push(new PONoCheckContext()); obligations.add(new StateInvariantObligation(this, ctxt)); - ctxt.pop(); } if (!isConstructor && !TypeComparator.isSubType(actualResult, type.result)) { - ctxt.push(new PONoCheckContext()); - obligations.add(new SubTypeObligation(this, actualResult, ctxt)); - ctxt.pop(); + obligations.add(new SubTypeObligation(this, actualResult, ctxt). + markUnchecked(ProofObligation.NOT_YET_SUPPORTED)); } } else @@ -224,8 +259,8 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment if (postcondition != null && Settings.dialect == Dialect.VDM_SL && Settings.release == Release.VDM_10) // Uses obj_C pattern { - ctxt.push(new POOperationDefinitionContext(this, false, state, false)); - obligations.add(new SatisfiabilityObligation(this, state, ctxt)); + ctxt.push(new POOperationDefinitionContext(this, false, stateDefinition, false)); + obligations.add(new SatisfiabilityObligation(this, stateDefinition, ctxt)); ctxt.pop(); } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/visitors/PODefinitionStateFinder.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/visitors/PODefinitionStateFinder.java index 302f4394e..022294de4 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/visitors/PODefinitionStateFinder.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/visitors/PODefinitionStateFinder.java @@ -25,6 +25,7 @@ package com.fujitsu.vdmj.po.definitions.visitors; import com.fujitsu.vdmj.po.POVisitorSet; +import com.fujitsu.vdmj.po.definitions.POAssignmentDefinition; import com.fujitsu.vdmj.po.definitions.PODefinition; import com.fujitsu.vdmj.tc.lex.TCNameSet; import com.fujitsu.vdmj.tc.lex.TCNameToken; @@ -39,6 +40,16 @@ public PODefinitionStateFinder(POVisitorSet vis this.visitorSet = visitors; } + @Override + public TCNameSet caseAssignmentDefinition(POAssignmentDefinition node, Boolean updates) + { + TCNameSet all = newCollection(); + + all.add(node.name); // eg. dcl declarations. + + return all; + } + @Override protected TCNameSet newCollection() { 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 56107ad78..8c4e8c737 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.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.lex.TCNameList; import com.fujitsu.vdmj.tc.types.TCType; @@ -100,7 +101,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment if (!hidden.isEmpty()) { - _obligations.markUnchecked("Obligation patterns contain hidden variables: " + hidden); + _obligations.markUnchecked(ProofObligation.HIDDEN_VARIABLES + ": " + hidden); } obligations.addAll(_obligations); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAlwaysStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAlwaysStatement.java index ca154a750..fcfeea6a9 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAlwaysStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAlwaysStatement.java @@ -27,7 +27,6 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor; import com.fujitsu.vdmj.pog.POContextStack; -import com.fujitsu.vdmj.pog.PONoCheckContext; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -54,10 +53,7 @@ public String toString() @Override public ProofObligationList getProofObligations(POContextStack ctxt, POContextStack globals, Environment env) { - ctxt.push(new PONoCheckContext()); ProofObligationList obligations = always.getProofObligations(ctxt, globals, env); - ctxt.pop(); - obligations.addAll(body.getProofObligations(ctxt, globals, env)); return obligations; } 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 3fc5d8439..afa37109f 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 @@ -29,6 +29,7 @@ import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor; import com.fujitsu.vdmj.pog.POContextStack; import com.fujitsu.vdmj.pog.POScopeContext; +import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -55,7 +56,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POContextSta if (!assignmentDefs.isEmpty()) { - obligations.markUnchecked("dcl statement block"); + obligations.markUnchecked(ProofObligation.DCL_STATEMENT); } return obligations; 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 d7546a039..71cfa5b48 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 @@ -29,6 +29,7 @@ import com.fujitsu.vdmj.po.patterns.POPattern; import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -59,7 +60,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POContextSta { ProofObligationList obligations = set.getProofObligations(ctxt, env); obligations.addAll(statement.getProofObligations(ctxt, globals, env)); - obligations.markUnchecked("Loop statement"); + obligations.markUnchecked(ProofObligation.LOOP_STATEMENT); 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 095b3e133..2a2c51c3e 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 @@ -29,6 +29,7 @@ import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor; import com.fujitsu.vdmj.pog.POContextStack; import com.fujitsu.vdmj.pog.POScopeContext; +import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.lex.TCNameToken; import com.fujitsu.vdmj.typechecker.Environment; @@ -75,7 +76,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POContextSta obligations.addAll(statement.getProofObligations(ctxt, globals, env)); ctxt.pop(); - obligations.markUnchecked("Loop statement"); + obligations.markUnchecked(ProofObligation.LOOP_STATEMENT); return obligations; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POSimpleBlockStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POSimpleBlockStatement.java index 21770d820..984c89a04 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POSimpleBlockStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POSimpleBlockStatement.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -68,10 +69,23 @@ public String toString() public ProofObligationList getProofObligations(POContextStack ctxt, POContextStack globals, Environment env) { ProofObligationList obligations = new ProofObligationList(); + boolean hasUpdatedState = false; for (POStatement stmt: statements) { - obligations.addAll(stmt.getProofObligations(ctxt, globals, env)); + ProofObligationList oblist = stmt.getProofObligations(ctxt, globals, env); + + if (stmt.updatesState()) + { + hasUpdatedState = true; + oblist.markUnchecked(ProofObligation.BODY_UPDATES_STATE); + } + else if (stmt.readsState() && hasUpdatedState) + { + oblist.markUnchecked(ProofObligation.HAS_UPDATED_STATE); + } + + obligations.addAll(oblist); } return obligations; 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 da0340931..2df437908 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 @@ -31,7 +31,6 @@ import com.fujitsu.vdmj.po.patterns.POTypeBind; import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor; import com.fujitsu.vdmj.pog.POContextStack; -import com.fujitsu.vdmj.pog.PONoCheckContext; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.SeqMemberObligation; import com.fujitsu.vdmj.pog.SetMemberObligation; @@ -87,10 +86,7 @@ else if (patternBind.bind instanceof POSeqBind) list.add(new SeqMemberObligation(bind.pattern.getMatchingExpression(), bind.sequence, ctxt)); } - ctxt.push(new PONoCheckContext()); list.addAll(with.getProofObligations(ctxt, globals, env)); - ctxt.pop(); - list.addAll(body.getProofObligations(ctxt, globals, env)); return list; } 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 f010b44d5..ea9814e75 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 @@ -28,6 +28,7 @@ import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.WhileLoopObligation; import com.fujitsu.vdmj.typechecker.Environment; @@ -58,7 +59,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POContextSta obligations.add(new WhileLoopObligation(this, ctxt)); obligations.addAll(exp.getProofObligations(ctxt, env)); obligations.addAll(statement.getProofObligations(ctxt, globals, env)); - obligations.markUnchecked("Loop statement"); + obligations.markUnchecked(ProofObligation.LOOP_STATEMENT); return obligations; } 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 951302cc3..952e33022 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 @@ -110,7 +110,7 @@ public TCNameSet caseCallObjectStatement(POCallObjectStatement node, Boolean upd @Override public TCNameSet caseLetDefStatement(POLetDefStatement node, Boolean updates) { - TCNameSet all = newCollection(); + TCNameSet all = super.caseLetDefStatement(node, updates); for (PODefinition def: node.localDefs) { @@ -128,7 +128,6 @@ public TCNameSet caseLetDefStatement(POLetDefStatement node, Boolean updates) } } - all.addAll(super.caseLetDefStatement(node, updates)); return all; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/OperationPostConditionObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/OperationPostConditionObligation.java index d73471fb0..89a98ff55 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/OperationPostConditionObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/OperationPostConditionObligation.java @@ -38,6 +38,7 @@ public OperationPostConditionObligation( { super(op.location, POType.OP_POST_CONDITION, ctxt); source = ctxt.getSource(getExp(op.precondition, op.postcondition, null)); + markUnchecked(ProofObligation.NOT_YET_SUPPORTED); } public OperationPostConditionObligation( @@ -45,6 +46,7 @@ public OperationPostConditionObligation( { super(op.location, POType.OP_POST_CONDITION, ctxt); source = ctxt.getSource(getExp(op.precondition, op.postcondition, op.errors)); + markUnchecked(ProofObligation.NOT_YET_SUPPORTED); } private String getExp(POExpression preexp, POExpression postexp, List errs) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java index b44470d97..11dca4fab 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java @@ -56,23 +56,6 @@ public String getName() return result.toString(); } - - public boolean isCheckable() - { - ListIterator p = this.listIterator(size()); - - while (p.hasPrevious()) - { - POContext c = p.previous(); - - if (c instanceof PONoCheckContext) - { - return false; - } - } - - return true; - } public String getSource(String poSource) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLetDefContext.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLetDefContext.java index 90626b8bc..39d7c0d0c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLetDefContext.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLetDefContext.java @@ -24,8 +24,11 @@ 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; +import com.fujitsu.vdmj.po.definitions.POValueDefinition; +import com.fujitsu.vdmj.po.patterns.POIdentifierPattern; public class POLetDefContext extends POContext { @@ -42,6 +45,13 @@ public POLetDefContext(PODefinition localDef) this.localDefs.add(localDef); } + public POLetDefContext(POAssignmentDefinition dcl) + { + this.localDefs = new PODefinitionList(); + this.localDefs.add(new POValueDefinition(null, + new POIdentifierPattern(dcl.name), dcl.type, dcl.expression, dcl.expType, new PODefinitionList())); + } + @Override public boolean isScopeBoundary() { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/PONoCheckContext.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/PONoCheckContext.java deleted file mode 100644 index d1505b84e..000000000 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/PONoCheckContext.java +++ /dev/null @@ -1,34 +0,0 @@ -/******************************************************************************* - * - * 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; - -public class PONoCheckContext extends POContext -{ - @Override - public String getSource() - { - return ""; - } -} 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 e45bf9db1..7414b9731 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java @@ -46,6 +46,17 @@ abstract public class ProofObligation implements Comparable { + // Arguments for the markUnchecked method. + public static final String NOT_YET_SUPPORTED = "Not yet supported for operations"; + public static final String MISSING_MEASURE = "Obligation for missing measure function"; + public static final String UNCHECKED_VDMPP = "Unchecked in VDM++"; + public static final String HIDDEN_VARIABLES = "Obligation patterns contain hidden variables"; + public static final String REQUIRES_VDM10 = "Obigation requires VDM10"; + public static final String BODY_UPDATES_STATE = "Operation body updates state"; + public static final String LOOP_STATEMENT = "Loop statement encountered"; + public static final String DCL_STATEMENT = "Block contains dcl assignments"; + public static final String HAS_UPDATED_STATE = "Previous statements updated state"; + public final LexLocation location; public final POType kind; public final String name; @@ -76,7 +87,7 @@ public ProofObligation(LexLocation location, POType kind, POContextStack ctxt) this.status = POStatus.UNPROVED; this.definition = ctxt.getDefinition(); this.number = 0; - this.isCheckable = ctxt.isCheckable(); // Set false for operation POs + this.isCheckable = true; // Set false for some operation POs this.typeParams = ctxt.getTypeParams(); this.annotations = ctxt.getAnnotations(); this.counterexample = null; @@ -84,11 +95,6 @@ public ProofObligation(LexLocation location, POType kind, POContextStack ctxt) this.message = null; this.provedBy = null; - if (!isCheckable) - { - this.status = POStatus.UNCHECKED; // Implies unproved - } - POGetMatchingExpressionVisitor.init(); // Reset the "any" count, before PO creation } @@ -151,13 +157,15 @@ public void setMessage(String message) } /** - * This is used to mark obligations as unchecked, with a reason. + * This is used to mark obligations as unchecked, with a reason code. */ - public void markUnchecked(String message) + public ProofObligation markUnchecked(String message) { this.isCheckable = false; this.setStatus(POStatus.UNCHECKED); this.setMessage(message); + + return this; // Convenient for new XYZObligation().markUnchecked(REASON) } public boolean isExistential() 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 b88af5f9c..d500e965a 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java @@ -229,7 +229,7 @@ private void typeCheck(ProofObligation obligation, String mname, Environment env { // Probably an implicit missing measure iter.remove(); - obligation.markUnchecked("Obligation for missing measure function"); + obligation.markUnchecked(ProofObligation.MISSING_MEASURE); } break; @@ -261,13 +261,16 @@ private void typeCheck(ProofObligation obligation, String mname, Environment env } /** - * This is used by POG to mark obligations as unchecked, with a reason. + * This is used by POG to mark all obligations as unchecked, with a reason. Preferably, + * use the reason code string constants in ProofObligation. */ - public void markUnchecked(String message) + public ProofObligationList markUnchecked(String message) { for (ProofObligation obligation: this) { obligation.markUnchecked(message); } + + return this; // Convenient for getProofObligations(ctxt, env).markUnchecked("Some reason") } } 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 e407470d1..3ad626911 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInvariantObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInvariantObligation.java @@ -72,6 +72,7 @@ public StateInvariantObligation( sb.append(invDefs(def.classDefinition)); source = ctxt.getSource(sb.toString()); + markUnchecked(ProofObligation.UNCHECKED_VDMPP); } public StateInvariantObligation( @@ -86,6 +87,7 @@ public StateInvariantObligation( sb.append(invDefs(def.classDefinition)); source = ctxt.getSource(sb.toString()); + markUnchecked(ProofObligation.UNCHECKED_VDMPP); } public StateInvariantObligation( @@ -100,6 +102,7 @@ public StateInvariantObligation( sb.append(invDefs(def.classDefinition)); source = ctxt.getSource(sb.toString()); + markUnchecked(ProofObligation.UNCHECKED_VDMPP); } private String invDefs(POClassDefinition def) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/SubTypeObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/SubTypeObligation.java index 1e0f20d9a..fcc1318a2 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/SubTypeObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/SubTypeObligation.java @@ -175,6 +175,7 @@ public SubTypeObligation( new TCNameToken(def.location, def.name.getModule(), "RESULT"), null); source = ctxt.getSource(oneType(false, result, def.type.result, actualResult)); + markUnchecked(ProofObligation.NOT_YET_SUPPORTED); } public SubTypeObligation( diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCStateDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCStateDefinition.java index b3f46baa3..394462e23 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCStateDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCStateDefinition.java @@ -36,6 +36,7 @@ import com.fujitsu.vdmj.tc.types.TCField; import com.fujitsu.vdmj.tc.types.TCFieldList; import com.fujitsu.vdmj.tc.types.TCFunctionType; +import com.fujitsu.vdmj.tc.types.TCInvariantType; import com.fujitsu.vdmj.tc.types.TCRecordType; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.tc.types.TCTypeList; @@ -271,7 +272,9 @@ private TCExplicitFunctionDefinition getInvDefinition() parameters.add(params); TCTypeList ptypes = new TCTypeList(); - ptypes.add(new TCUnresolvedType(name)); + TCInvariantType param = recordType.copy(true); + ptypes.add(param); + // ptypes.add(new TCUnresolvedType(name)); TCFunctionType ftype = new TCFunctionType(loc, ptypes, false, new TCBooleanType(loc)); TCExplicitFunctionDefinition def = new TCExplicitFunctionDefinition(null, TCAccessSpecifier.DEFAULT, diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/values/SetValue.java b/vdmj/src/main/java/com/fujitsu/vdmj/values/SetValue.java index ba9cc7307..2aca04ca1 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/values/SetValue.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/values/SetValue.java @@ -86,10 +86,10 @@ public UpdatableValue getUpdatable(ValueListenerList listeners) for (Value k: values) { Value v = k.getUpdatable(listeners); - nset.add(v); + nset.addSorted(v, values.isSorted()); } - return UpdatableValue.factory(new SetValue(nset, false), listeners); + return UpdatableValue.factory(new SetValue(nset, !values.isSorted()), listeners); } @Override @@ -100,10 +100,10 @@ public Value getConstant() for (Value k: values) { Value v = k.getConstant(); - nset.add(v); + nset.addSorted(v, values.isSorted()); } - return new SetValue(nset, false); + return new SetValue(nset, !values.isSorted()); } @Override @@ -191,10 +191,10 @@ protected Value convertValueTo(TCType to, Context ctxt, TCTypeSet done) throws V for (Value v: values) { - ns.add(v.convertValueTo(setto.setof, ctxt)); + ns.addUnsorted(v.convertValueTo(setto.setof, ctxt)); } - return new SetValue(ns, true); // Re-sort, as ord_T may be different + return new SetValue(ns, true); // Re-sort, as new type's ord_T may be different } else { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/values/ValueSet.java b/vdmj/src/main/java/com/fujitsu/vdmj/values/ValueSet.java index 947b9027d..805db6fe0 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/values/ValueSet.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/values/ValueSet.java @@ -83,6 +83,11 @@ public ValueSet(Value ...values) add(v); } } + + public boolean isSorted() + { + return isSorted; + } @Override public boolean equals(Object other) @@ -90,7 +95,27 @@ public boolean equals(Object other) if (other instanceof ValueSet) { ValueSet os = (ValueSet)other; - return os.size() == size() && os.containsAll(this); + + if (os.size() != size()) + { + return false; + } + else if (isSorted && os.isSorted) + { + for (int i=0; i permutedSets() for (int i=0; i powerSet(Breakpoint breakpoint, Context ctxt) for (int i=0; i= 100) 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 748ca7294..c5e3426ea 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 & pre_op2(new A(iv)) =>\n while (x > 0) do ...)\n", - /* 85 */ "(forall obj_A(iv |-> iv):A & pre_op2(new A(iv)) =>\n let iv = (iv + 1) in (iv < 10))\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", }; public void testPOG() throws Exception