diff --git a/quickcheck/src/main/java/quickcheck/QuickCheck.java b/quickcheck/src/main/java/quickcheck/QuickCheck.java index 91833dc5e..dd8c529d7 100644 --- a/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -73,6 +73,7 @@ import quickcheck.strategies.QCStrategy; import quickcheck.strategies.StrategyResults; import quickcheck.visitors.FixedRangeCreator; +import quickcheck.visitors.MaybeFinder; import quickcheck.visitors.TypeBindFinder; public class QuickCheck @@ -399,7 +400,7 @@ else if (results.provedBy != null) if (values != null) { verbose("PO #%d, setting %s, %d values\n", po.number, mbind.toString(), values.size()); - mbind.setBindValues(values, timeout); + mbind.setBindValues(values, timeout, results.hasAllValues); } else { @@ -428,6 +429,7 @@ else if (results.provedBy != null) Value execResult = new BooleanValue(false); ContextException execException = null; boolean execCompleted = false; + boolean hasMaybe = false; long before = System.currentTimeMillis(); try @@ -442,6 +444,10 @@ else if (results.provedBy != null) { ictxt.next(); execResult = poexp.eval(ictxt); + + MaybeFinder finder = new MaybeFinder(); + poexp.apply(finder, null); + hasMaybe = finder.hasMaybe(); } while (ictxt.hasNext() && execResult.boolValue(ctxt)); @@ -502,6 +508,10 @@ else if (execResult instanceof BooleanValue) { outcome = POStatus.TIMEOUT; } + else if (hasMaybe) + { + outcome = POStatus.MAYBE; + } else if (po.isExistential()) { outcome = POStatus.PROVED; // An "exists" PO is PROVED, if true. @@ -540,6 +550,14 @@ else if (results.hasAllValues && execCompleted) po.setMessage(null); po.setWitness(null); } + else if (hasMaybe) + { + infof(POStatus.MAYBE, "PO #%d, MAYBE %s\n", po.number, duration(before, after)); + po.setStatus(POStatus.MAYBE); + po.setCounterexample(null); + po.setMessage(null); + po.setWitness(null); + } else if (po.isExistential()) // Principal exp is "exists..." { if (results.hasAllValues) @@ -615,7 +633,7 @@ else if (po.isExistential()) // Principal exp is "exists..." { for (INBindingSetter mbind: bindings) { - mbind.setBindValues(null, 0); // Clears everything + mbind.setBindValues(null, 0, false); // Clears everything } } } diff --git a/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java b/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java index a4eb814b0..054965c7e 100644 --- a/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java +++ b/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java @@ -90,7 +90,7 @@ public StrategyResults getValues(ProofObligation po, INExpression exp, List. + * SPDX-License-Identifier: GPL-3.0-or-later + * + ******************************************************************************/ +package quickcheck.visitors; + +import java.util.List; +import java.util.Vector; + +import com.fujitsu.vdmj.in.expressions.INExistsExpression; +import com.fujitsu.vdmj.in.expressions.INExpression; +import com.fujitsu.vdmj.in.expressions.INForAllExpression; +import com.fujitsu.vdmj.in.expressions.visitors.INLeafExpressionVisitor; + +/** + * Search an expression tree after a QuickCheck execution to decide the outcome. + * This is affected by the forall/exists subexpressions, whether they have + * type bindings set and whether the binds have all type values. + */ +public class MaybeFinder extends INLeafExpressionVisitor, Object> +{ + private int maybeCount = 0; + + public MaybeFinder() + { + super(false); + } + + public boolean hasMaybe() + { + return maybeCount > 0; + } + + @Override + protected List newCollection() + { + return new Vector(); + } + + @Override + public List caseExpression(INExpression node, Object arg) + { + return newCollection(); + } + + @Override + public List caseForAllExpression(INForAllExpression node, Object arg) + { + if (node.maybe) + { + maybeCount++; + node.maybe = false; + } + + return super.caseForAllExpression(node, arg); + } + + @Override + public List caseExistsExpression(INExistsExpression node, Object arg) + { + if (node.maybe) + { + maybeCount++; + node.maybe = false; + } + + return super.caseExistsExpression(node, arg); + } +} diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INExistsExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INExistsExpression.java index 6dce6eb75..9c2f4dee6 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INExistsExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INExistsExpression.java @@ -24,7 +24,6 @@ package com.fujitsu.vdmj.in.expressions; import com.fujitsu.vdmj.in.expressions.visitors.INExpressionVisitor; -import com.fujitsu.vdmj.in.patterns.INBindingSetter; import com.fujitsu.vdmj.in.patterns.INMultipleBind; import com.fujitsu.vdmj.in.patterns.INMultipleBindList; import com.fujitsu.vdmj.in.patterns.INPattern; @@ -44,6 +43,9 @@ public class INExistsExpression extends INExpression private static final long serialVersionUID = 1L; public final INMultipleBindList bindList; public final INExpression predicate; + + /** True if the execution did not have all bind values on exit */ + public boolean maybe = false; public INExistsExpression(LexLocation location, INMultipleBindList bindList, INExpression predicate) { @@ -63,7 +65,7 @@ public Value eval(Context ctxt) { breakpoint.check(location, ctxt); long start = System.currentTimeMillis(); - long timeout = getTimeout(); + long timeout = bindList.getTimeout(); try { @@ -88,7 +90,8 @@ public Value eval(Context ctxt) { if (System.currentTimeMillis() - start > timeout) { - setCounterexample(null, true); + bindList.setCounterexample(null, true); + maybe = true; return new BooleanValue(true); } } @@ -109,7 +112,6 @@ public Value eval(Context ctxt) { if (!v.equals(nvp.value)) { - setWitness(evalContext); matches = false; break; // This quantifier set does not match } @@ -120,7 +122,8 @@ public Value eval(Context ctxt) { if (matches && predicate.eval(evalContext).boolValue(ctxt)) { - setWitness(evalContext); + bindList.setWitness(evalContext); + maybe = false; return new BooleanValue(true); } } @@ -135,71 +138,10 @@ public Value eval(Context ctxt) abort(e); } + maybe = !bindList.hasAllValues(); return new BooleanValue(false); } - - /** - * This is used by the QuickCheck plugin to limit PO execution times. - */ - private long getTimeout() - { - for (INMultipleBind bind: bindList) - { - if (bind instanceof INBindingSetter) // Type and multitype binds - { - INBindingSetter setter = (INBindingSetter)bind; - long timeout = setter.getTimeout(); - - if (timeout > 0) - { - return timeout; - } - } - } - - return 0; - } - - /** - * This is used by the QuickCheck plugin to report which values failed. - */ - private void setCounterexample(Context ctxt, boolean didTimeout) - { - for (INMultipleBind bind: bindList) - { - if (bind instanceof INBindingSetter) // Type and multitype binds - { - INBindingSetter setter = (INBindingSetter)bind; - - if (setter.getBindValues() != null) // One we care about (set QC values for) - { - setter.setCounterexample(ctxt, didTimeout); - break; // Just one will do - see QC printFailPath - } - } - } - } - - /** - * This is used by the QuickCheck plugin to report which values succeeded. - */ - private void setWitness(Context ctxt) - { - for (INMultipleBind bind: bindList) - { - if (bind instanceof INBindingSetter) // Type and multitype binds - { - INBindingSetter setter = (INBindingSetter)bind; - - if (setter.getBindValues() != null) // One we care about (set QC values for) - { - setter.setWitness(ctxt); - break; // Just one will do - see QC printFailPath - } - } - } - } - + @Override public R apply(INExpressionVisitor visitor, S arg) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INForAllExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INForAllExpression.java index d3a0b6236..c63d6da21 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INForAllExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INForAllExpression.java @@ -25,7 +25,6 @@ package com.fujitsu.vdmj.in.expressions; import com.fujitsu.vdmj.in.expressions.visitors.INExpressionVisitor; -import com.fujitsu.vdmj.in.patterns.INBindingSetter; import com.fujitsu.vdmj.in.patterns.INMultipleBind; import com.fujitsu.vdmj.in.patterns.INMultipleBindList; import com.fujitsu.vdmj.in.patterns.INPattern; @@ -48,6 +47,9 @@ public class INForAllExpression extends INExpression public final INMultipleBindList bindList; public final INExpression predicate; + /** True if the execution did not have all bind values on exit */ + public boolean maybe = false; + public INForAllExpression(LexLocation location, INMultipleBindList bindList, INExpression predicate) { super(location); @@ -66,7 +68,7 @@ public Value eval(Context ctxt) { breakpoint.check(location, ctxt); long start = System.currentTimeMillis(); - long timeout = getTimeout(); + long timeout = bindList.getTimeout(); try { @@ -91,7 +93,8 @@ public Value eval(Context ctxt) { if (System.currentTimeMillis() - start > timeout) { - setCounterexample(null, true); + bindList.setCounterexample(null, true); + maybe = true; return new BooleanValue(true); } } @@ -122,13 +125,15 @@ public Value eval(Context ctxt) { if (matches && !predicate.eval(evalContext).boolValue(ctxt)) { - setCounterexample(evalContext, false); + bindList.setCounterexample(evalContext, false); + maybe = !bindList.hasAllValues(); return new BooleanValue(false); } } catch (ContextException e) { - setCounterexample(evalContext, false); + bindList.setCounterexample(evalContext, false); + maybe = !bindList.hasAllValues(); throw e; } catch (ValueException e) @@ -142,51 +147,10 @@ public Value eval(Context ctxt) return abort(e); } + maybe = !bindList.hasAllValues(); return new BooleanValue(true); } - - /** - * This is used by the QuickCheck plugin to limit PO execution times. - */ - private long getTimeout() - { - for (INMultipleBind bind: bindList) - { - if (bind instanceof INBindingSetter) // Type and multitype binds - { - INBindingSetter setter = (INBindingSetter)bind; - long timeout = setter.getTimeout(); - - if (timeout > 0) - { - return timeout; - } - } - } - - return 0; - } - - /** - * This is used by the QuickCheck plugin to report which values failed. - */ - private void setCounterexample(Context ctxt, boolean didTimeout) - { - for (INMultipleBind bind: bindList) - { - if (bind instanceof INBindingSetter) // Type and multitype binds - { - INBindingSetter setter = (INBindingSetter)bind; - - if (setter.getBindValues() != null) // One we care about (set QC values for) - { - setter.setCounterexample(ctxt, didTimeout); - break; // Just one will do - see QC printFailPath - } - } - } - } - + @Override public R apply(INExpressionVisitor visitor, S arg) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INBindingSetter.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INBindingSetter.java index 6adbc0b02..22cccff52 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INBindingSetter.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INBindingSetter.java @@ -30,8 +30,9 @@ public interface INBindingSetter { - public void setBindValues(ValueList values, long timeout); + public void setBindValues(ValueList values, long timeout, boolean hasAllValues); public ValueList getBindValues(); + public boolean hasAllValues(); public long getTimeout(); public boolean didTimeout(); public TCType getType(); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INMultipleBindList.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INMultipleBindList.java index 09b4207ca..3525c7657 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INMultipleBindList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INMultipleBindList.java @@ -25,6 +25,7 @@ package com.fujitsu.vdmj.in.patterns; import com.fujitsu.vdmj.in.INMappedList; +import com.fujitsu.vdmj.runtime.Context; import com.fujitsu.vdmj.tc.patterns.TCMultipleBind; import com.fujitsu.vdmj.tc.patterns.TCMultipleBindList; @@ -41,4 +42,105 @@ public INMultipleBindList(TCMultipleBindList from) throws Exception { super(from); } + + /** + * QuickCheck has set some type binds? + */ + public boolean isInstrumented() + { + for (INMultipleBind bind: this) + { + if (bind instanceof INBindingSetter) // Type and multitype binds + { + INBindingSetter setter = (INBindingSetter)bind; + + if (setter.getBindValues() != null) + { + return true; + } + } + } + + return false; + } + + /** + * This is used by the QuickCheck plugin to limit PO execution times. + */ + public long getTimeout() + { + for (INMultipleBind bind: this) + { + if (bind instanceof INBindingSetter) // Type and multitype binds + { + INBindingSetter setter = (INBindingSetter)bind; + long timeout = setter.getTimeout(); + + if (timeout > 0) + { + return timeout; + } + } + } + + return 0; + } + + /** + * This is used by the QuickCheck plugin to report which values failed. + */ + public void setCounterexample(Context ctxt, boolean didTimeout) + { + for (INMultipleBind bind: this) + { + if (bind instanceof INBindingSetter) // Type and multitype binds + { + INBindingSetter setter = (INBindingSetter)bind; + + if (setter.getBindValues() != null) // One we care about (set QC values for) + { + setter.setCounterexample(ctxt, didTimeout); + break; // Just one will do - see QC printFailPath + } + } + } + } + + /** + * This is used by the QuickCheck plugin to report which values succeeded. + */ + public void setWitness(Context ctxt) + { + for (INMultipleBind bind: this) + { + if (bind instanceof INBindingSetter) // Type and multitype binds + { + INBindingSetter setter = (INBindingSetter)bind; + + if (setter.getBindValues() != null) // One we care about (set QC values for) + { + setter.setWitness(ctxt); + break; // Just one will do - see QC printFailPath + } + } + } + } + + public boolean hasAllValues() + { + for (INMultipleBind bind: this) + { + if (bind instanceof INBindingSetter) // Type and multitype binds + { + INBindingSetter setter = (INBindingSetter)bind; + + if (!setter.hasAllValues()) + { + return false; // One hasn't + } + } + } + + return true; // All have + } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INMultipleTypeBind.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INMultipleTypeBind.java index 2fb850f3f..082c92edf 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INMultipleTypeBind.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INMultipleTypeBind.java @@ -47,6 +47,7 @@ public class INMultipleTypeBind extends INMultipleBind implements INBindingSette private Context bindWitness = null; private boolean bindPermuted = false; private boolean bindOverride = false; + private boolean bindAllValues = false; private long bindTimeout = 0; private boolean didTimeout = false; @@ -64,13 +65,14 @@ public String toString() } @Override - public void setBindValues(ValueList values, long timeout) + public void setBindValues(ValueList values, long timeout, boolean hasAllValues) { if (values == null) { bindValues = null; bindOverride = false; bindTimeout = 0; + bindAllValues = true; // NOTE: because execution usually does } else { @@ -78,6 +80,7 @@ public void setBindValues(ValueList values, long timeout) bindValues.addAll(values); bindOverride = true; bindTimeout = timeout; + bindAllValues = hasAllValues; } didTimeout = false; @@ -102,6 +105,12 @@ public boolean didTimeout() { return didTimeout; } + + @Override + public boolean hasAllValues() + { + return bindAllValues; + } @Override public void setCounterexample(Context ctxt, boolean didTimeout) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INTypeBind.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INTypeBind.java index 92b1d3f33..1d70c7e55 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INTypeBind.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INTypeBind.java @@ -47,6 +47,7 @@ public class INTypeBind extends INBind implements INBindingSetter private Context bindWitness = null; private boolean bindPermuted = false; private boolean bindOverride = false; + private boolean bindAllValues = false; private long bindTimeout = 0; private boolean didTimeout = false; @@ -58,13 +59,14 @@ public INTypeBind(INPattern pattern, TCType type) } @Override - public void setBindValues(ValueList values, long timeout) + public void setBindValues(ValueList values, long timeout, boolean hasAllValues) { if (values == null) { bindValues = null; bindOverride = false; bindTimeout = 0; + bindAllValues = true; // NOTE: because execution usually does } else { @@ -72,6 +74,7 @@ public void setBindValues(ValueList values, long timeout) bindValues.addAll(values); bindOverride = true; bindTimeout = timeout; + bindAllValues = hasAllValues; } didTimeout = false; @@ -96,6 +99,12 @@ public boolean didTimeout() { return didTimeout; } + + @Override + public boolean hasAllValues() + { + return bindAllValues; + } @Override public TCType getType() 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 09cc8172c..ee49f7764 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 @@ -137,8 +137,6 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment (annotations != null) ? annotations.poBefore(this, ctxt) : new ProofObligationList(); TCNameList pids = new TCNameList(); boolean matchNeeded = false; - - ctxt.push(new PONoCheckContext()); for (POPatternListTypePair pltp: parameterPatterns) { @@ -178,11 +176,14 @@ 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) { + ctxt.push(new PONoCheckContext()); obligations.addAll(body.getProofObligations(ctxt, env)); if (isConstructor && @@ -195,23 +196,21 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment if (!isConstructor && !TypeComparator.isSubType(actualResult, type.result)) { - obligations.add( - new SubTypeObligation(this, actualResult, ctxt)); + obligations.add(new SubTypeObligation(this, actualResult, ctxt)); } + + ctxt.pop(); } else { if (postcondition != null) { ctxt.push(new POOperationDefinitionContext(this, false, state)); - obligations.add( - new SatisfiabilityObligation(this, state, ctxt)); + obligations.add(new SatisfiabilityObligation(this, state, ctxt)); ctxt.pop(); } } - ctxt.pop(); - if (annotations != null) annotations.poAfter(this, obligations, ctxt); return obligations; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/PORemoveIgnoresVisitor.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/PORemoveIgnoresVisitor.java index 35e09fc72..e17a40a2c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/PORemoveIgnoresVisitor.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/PORemoveIgnoresVisitor.java @@ -94,6 +94,15 @@ public POPattern caseExpressionPattern(POExpressionPattern node, Object arg) @Override public POPattern caseIdentifierPattern(POIdentifierPattern node, Object arg) { + // If we encounter any "old" state names, like "Sigma~", we rename to + // "oldSigma" to allow POs to work as simple expressions. + + if (node.name.isOld()) + { + TCNameToken oldName = new TCNameToken(node.location, node.location.module, "old" + node.name.getName()); + return new POIdentifierPattern(oldName); + } + return node; } 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 69f586dc2..18dcf32f7 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java @@ -136,44 +136,6 @@ public PODefinition getDefinition() return null; } - public boolean isExistential() - { - for (POContext ctxt: this) - { - if (ctxt instanceof PONameContext || - ctxt instanceof PONoCheckContext || - ctxt instanceof POScopeContext) - { - continue; // These aren't important - } - else - { - return ctxt.isExistential(); - } - } - - return false; - } - - public boolean hasNone() - { - for (POContext ctxt: this) - { - if (ctxt instanceof PONameContext || - ctxt instanceof PONoCheckContext || - ctxt instanceof POScopeContext) - { - continue; // These aren't important - } - else - { - return false; // Has something significant - } - } - - return true; // Has nothing important - } - public TCTypeList getTypeParams() { for (POContext ctxt: this) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POImpliesContext.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POImpliesContext.java index 355355ec6..08185acb7 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POImpliesContext.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POImpliesContext.java @@ -39,12 +39,12 @@ public POImpliesContext(POExpression precondition) public POImpliesContext(POExplicitOperationDefinition def) { - this.exp = preconditionCall(def.name, null, def.getParamPatternList(), def.precondition); + this.exp = preconditionCall(def.name, null, def.predef.getParamPatternList(), def.precondition); } public POImpliesContext(POImplicitOperationDefinition def) { - this.exp = preconditionCall(def.name, null, def.getParamPatternList(), def.precondition); + this.exp = preconditionCall(def.name, null, def.predef.getParamPatternList(), def.precondition); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POOperationDefinitionContext.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POOperationDefinitionContext.java index f2a0246be..e4ae1891c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POOperationDefinitionContext.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POOperationDefinitionContext.java @@ -61,7 +61,7 @@ public String getContext() { StringBuilder sb = new StringBuilder(); - if (!deftype.parameters.isEmpty()) + if (!deftype.parameters.isEmpty() || stateDefinition != null) { sb.append("forall "); String sep = ""; @@ -78,6 +78,7 @@ public String getContext() if (stateDefinition != null) { + sb.append(sep); appendStatePatterns(sb); } @@ -103,13 +104,13 @@ private void appendStatePatterns(StringBuilder sb) else if (stateDefinition instanceof POStateDefinition) { POStateDefinition def = (POStateDefinition)stateDefinition; - sb.append(", oldstate:"); + sb.append("oldstate:"); sb.append(def.name.getName()); } else { POClassDefinition def = (POClassDefinition)stateDefinition; - sb.append(", oldself:"); + sb.append("oldself:"); sb.append(def.name.getName()); } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POType.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POType.java index 7a7bfab80..05d891a61 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POType.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POType.java @@ -30,9 +30,9 @@ public enum POType FUNC_APPLY("function apply"), SEQ_APPLY("sequence apply"), FUNC_POST_CONDITION("post condition"), - FUNC_SATISFIABILITY("function satisfiability", true), - FUNC_PATTERNS("function parameter patterns", true), - LET_BE_EXISTS("let be st existence", true), + FUNC_SATISFIABILITY("function satisfiability"), + FUNC_PATTERNS("function parameter patterns"), + LET_BE_EXISTS("let be st existence"), UNIQUE_EXISTENCE("unique existence binding"), // Note: not existential! FUNC_ITERATION("function iteration"), MAP_ITERATION("map iteration"), @@ -41,13 +41,13 @@ public enum POType NON_EMPTY_SET("non-empty set"), NON_EMPTY_SEQ("non-empty sequence"), NON_ZERO("non-zero"), - FINITE_MAP("finite map", true), - FINITE_SET("finite set", true), + FINITE_MAP("finite map"), + FINITE_SET("finite set"), MAP_COMPATIBLE("map compatible"), MAP_SEQ_OF_COMPATIBLE("map sequence compatible"), MAP_SET_OF_COMPATIBLE("map set compatible"), SEQ_MODIFICATION("sequence modification"), - VALUE_BINDING("value binding", true), + VALUE_BINDING("value binding"), SUB_TYPE("subtype"), CASES_EXHAUSTIVE("cases exhaustive"), INVARIANT("type invariant"), @@ -55,7 +55,7 @@ public enum POType STATE_INVARIANT("state invariant"), WHILE_LOOP("while loop termination"), OP_POST_CONDITION("operation post condition"), - OPERATION_PATTERNS("operation parameter patterns", true), + OPERATION_PATTERNS("operation parameter patterns"), OP_SATISFIABILITY("operation satisfiability"), SET_MEMBER("set membership"), SEQ_MEMBER("sequence membership"), @@ -64,30 +64,17 @@ public enum POType TOTAL_ORDER("total order"), EQUIV_RELATION("equivalence relation"), TOTAL("total function"), - INV_SATISFIABILITY("invariant satisfiability", true), + INV_SATISFIABILITY("invariant satisfiability"), THEOREM("theorem"), - STATE_INIT("state init", true); + STATE_INIT("state init"); private String kind; - private boolean existential; // PO is of the form "exists ..." rather than "forall ..." etc. POType(String kind) { this.kind = kind; - this.existential = false; } - POType(String kind, boolean existential) - { - this.kind = kind; - this.existential = existential; - } - - public boolean isExistential() - { - return existential; - } - @Override public String toString() { 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 6846878df..f761c4704 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java @@ -37,6 +37,7 @@ import com.fujitsu.vdmj.po.patterns.visitors.PORemoveIgnoresVisitor; import com.fujitsu.vdmj.po.types.POPatternListTypePair; import com.fujitsu.vdmj.runtime.Context; +import com.fujitsu.vdmj.tc.expressions.TCExistsExpression; import com.fujitsu.vdmj.tc.expressions.TCExpression; import com.fujitsu.vdmj.tc.types.TCParameterType; import com.fujitsu.vdmj.tc.types.TCType; @@ -86,7 +87,7 @@ public ProofObligation(LexLocation location, POType kind, POContextStack ctxt) this.status = POStatus.UNCHECKED; // Implies unproved } - existential = ctxt.isExistential() || (ctxt.hasNone() && kind.isExistential()); + //existential = ctxt.isExistential() || (ctxt.hasNone() && kind.isExistential()); POGetMatchingExpressionVisitor.init(); // Reset the "any" count, before PO creation } @@ -203,6 +204,7 @@ public int compareTo(ProofObligation other) public void setCheckedExpression(TCExpression checkedExpression) { this.checkedExpression = checkedExpression; + this.existential = (checkedExpression instanceof TCExistsExpression); } public TCExpression getCheckedExpression() diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/SatisfiabilityObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/SatisfiabilityObligation.java index ff83f4b83..a2d33d76e 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/SatisfiabilityObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/SatisfiabilityObligation.java @@ -93,6 +93,7 @@ public SatisfiabilityObligation(POImplicitOperationDefinition op, separator = ""; appendResult(sb, op.result); appendStatePatterns(sb, stateDefinition, false, true); + appendStatePatterns(sb, stateDefinition, true, true); sb.append(" & "); }