From 20d108053adee1eeda3fe4cf56ca94526610fc72 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Tue, 7 Nov 2023 15:09:48 +0000 Subject: [PATCH 1/3] Correctly set the polymorphic types of measures and their pre's --- .../in/definitions/INExplicitFunctionDefinition.java | 11 +++++++++++ .../in/definitions/INImplicitFunctionDefinition.java | 11 +++++++++++ .../java/com/fujitsu/vdmj/values/FunctionValue.java | 9 +++++++++ 3 files changed, 31 insertions(+) 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/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 From 251652268ae9c9e11b01724fd7d03ae9bbdeadfc Mon Sep 17 00:00:00 2001 From: nick_battle Date: Tue, 7 Nov 2023 19:27:42 +0000 Subject: [PATCH 2/3] Add hasCorrelatedBinds for POs --- .../fujitsu/vdmj/pog/CasesExhaustiveObligation.java | 12 ++++++++++++ .../java/com/fujitsu/vdmj/pog/ProofObligation.java | 11 +++++++++++ 2 files changed, 23 insertions(+) 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() From 7c0c8b49481aad0359cea6711099adc393b9dd67 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Tue, 7 Nov 2023 19:28:44 +0000 Subject: [PATCH 3/3] Use PO.hasCorrelatedBinds and suppress function generation in creators --- .../strategies/RandomQCStrategy.java | 18 ++++++-- .../visitors/FixedRangeCreator.java | 9 +--- .../visitors/RandomRangeCreator.java | 3 +- .../quickcheck/visitors/RangeCreator.java | 46 +++++++++++++++++++ 4 files changed, 65 insertions(+), 11 deletions(-) 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); + } }