diff --git a/examples/quickcheck/src/main/java/quickcheck/strategies/RandomQCStrategy.java b/examples/quickcheck/src/main/java/quickcheck/strategies/RandomQCStrategy.java index 3fbd5cc3a..315e5913a 100644 --- a/examples/quickcheck/src/main/java/quickcheck/strategies/RandomQCStrategy.java +++ b/examples/quickcheck/src/main/java/quickcheck/strategies/RandomQCStrategy.java @@ -39,6 +39,7 @@ import com.fujitsu.vdmj.values.ValueSet; import quickcheck.QuickCheck; +import quickcheck.visitors.FixedRangeCreator; import quickcheck.visitors.RandomRangeCreator; public class RandomQCStrategy extends QCStrategy @@ -136,10 +137,21 @@ public StrategyResults getValues(ProofObligation po, INExpression exp, List @@ -114,4 +128,36 @@ protected int leastPower(int n, int limit) return power; } + + /** + * Attempt to produce a function that matches a (possibly polymorphic) TCFunctionType. + */ + protected FunctionValue instantiate(TCFunctionType node) + { + INPatternList params = new INPatternList(); + INExpression body = null; + + // Resolve any @T types referred to in the type parameters + TCFunctionType ptype = (TCFunctionType) INInstantiate.instantiate(node, ctxt, ctxt); + + for (int i=1; i <= ptype.parameters.size(); i++) + { + params.add(new INIdentifierPattern(new TCNameToken(node.location, node.location.module, "p" + i))); + } + + if (ptype.result instanceof TCBooleanType) + { + body = new INBooleanLiteralExpression(new LexBooleanToken(true, node.location)); + } + else if (ptype.result instanceof TCNumericType) + { + body = new INIntegerLiteralExpression(new LexIntegerToken(1, node.location)); + } + else + { + body = new INUndefinedExpression(node.location); + } + + return new FunctionValue(node.location, "$qc_dummy", ptype, params, body, null); + } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INExplicitFunctionDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INExplicitFunctionDefinition.java index 2b466bc89..20d0c4108 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INExplicitFunctionDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INExplicitFunctionDefinition.java @@ -177,6 +177,7 @@ public FunctionValue getPolymorphicValue(TCTypeList argTypes, Context params, Co FunctionValue prefv = null; FunctionValue postfv = null; + FunctionValue measurefv = null; if (predef != null) { @@ -188,9 +189,19 @@ public FunctionValue getPolymorphicValue(TCTypeList argTypes, Context params, Co postfv = postdef.getPolymorphicValue(argTypes, params, ctxt); } + if (measureDef != null) + { + measurefv = measureDef.getPolymorphicValue(argTypes, params, ctxt); + } + TCFunctionType ftype = (TCFunctionType)INInstantiate.instantiate(getType(), params, ctxt); FunctionValue rv = new FunctionValue(this, ftype, params, prefv, postfv, null); + if (measurefv != null) + { + rv.setMeasure(measurefv); + } + polyfuncs.put(argTypes, rv); return rv; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INImplicitFunctionDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INImplicitFunctionDefinition.java index 2a07b71c1..bcd810665 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INImplicitFunctionDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INImplicitFunctionDefinition.java @@ -189,6 +189,7 @@ public FunctionValue getPolymorphicValue(TCTypeList actualTypes, Context params, FunctionValue prefv = null; FunctionValue postfv = null; + FunctionValue measurefv = null; if (predef != null) { @@ -199,10 +200,20 @@ public FunctionValue getPolymorphicValue(TCTypeList actualTypes, Context params, { postfv = postdef.getPolymorphicValue(actualTypes, params, ctxt); } + + if (measureDef != null) + { + measurefv = measureDef.getPolymorphicValue(actualTypes, params, ctxt); + } TCFunctionType ftype = (TCFunctionType)INInstantiate.instantiate(getType(), params, ctxt); FunctionValue rv = new FunctionValue(this, ftype, params, prefv, postfv, null); + if (measurefv != null) + { + rv.setMeasure(measurefv); + } + polyfuncs.put(actualTypes, rv); return rv; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/CasesExhaustiveObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/CasesExhaustiveObligation.java index c1093ddbd..97ecbbefb 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/CasesExhaustiveObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/CasesExhaustiveObligation.java @@ -30,11 +30,14 @@ public class CasesExhaustiveObligation extends ProofObligation { + private final boolean hasCorrelatedBinds; + public CasesExhaustiveObligation(POCasesExpression exp, POContextStack ctxt) { super(exp.location, POType.CASES_EXHAUSTIVE, ctxt); StringBuilder sb = new StringBuilder(); String prefix = ""; + boolean correlated = false; for (POCaseAlternative alt: exp.cases) { @@ -59,11 +62,20 @@ public CasesExhaustiveObligation(POCasesExpression exp, POContextStack ctxt) sb.append(" = "); sb.append(alt.pattern.removeIgnorePatterns()); sb.append(")"); + + correlated = true; } prefix = " or "; } + hasCorrelatedBinds = correlated; value = ctxt.getObligation(sb.toString()); } + + @Override + public boolean hasCorrelatedBinds() + { + return hasCorrelatedBinds; + } } 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 865478690..3a1c413b1 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java @@ -118,6 +118,17 @@ public boolean isExistential() { return existential; } + + /** + * True if there are multiple binds in the obligation which represent "the same" values, + * for example a forall x:nat... with an exists y:nat.. inside that is reasoning about + * the same set of nats. In this case, the random strategy has to include fixed values + * too. + */ + public boolean hasCorrelatedBinds() + { + return false; + } @Override public String toString() diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/values/FunctionValue.java b/vdmj/src/main/java/com/fujitsu/vdmj/values/FunctionValue.java index 1fa87d805..b9a971c77 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/values/FunctionValue.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/values/FunctionValue.java @@ -248,6 +248,15 @@ public void setSelf(ObjectValue self) } } } + + public void setMeasure(FunctionValue measure) + { + measure.measuringThreads = Collections.synchronizedSet(new HashSet()); + measure.callingThreads = Collections.synchronizedSet(new HashSet()); + measure.isMeasure = true; + + this.measure = measure; + } public Value eval( LexLocation from, Value arg, Context ctxt) throws ValueException