From 1a9286c2afa54d23d72fff2573c1ef775147df42 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Sat, 4 Nov 2023 23:09:38 +0000 Subject: [PATCH 1/4] Look for duplicate POs in ProofObligationList add/AddAll --- .../com/fujitsu/vdmj/pog/ProofObligation.java | 12 +++++++++ .../fujitsu/vdmj/pog/ProofObligationList.java | 25 +++++++++++++++++++ 2 files changed, 37 insertions(+) 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 f032bca85..e4e935a6e 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java @@ -120,6 +120,18 @@ public String toString() return sb.toString(); } + + @Override + public boolean equals(Object other) + { + if (other instanceof ProofObligation) + { + ProofObligation opo = (ProofObligation)other; + return kind == opo.kind && location == opo.location; + } + + return false; + } protected String getVar(String root) { 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 318783ac6..f96a76c6f 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java @@ -24,6 +24,7 @@ package com.fujitsu.vdmj.pog; +import java.util.Collection; import java.util.Iterator; import java.util.List; import java.util.Vector; @@ -55,6 +56,30 @@ public class ProofObligationList extends Vector { // Convenience class to hold lists of POs. + + @Override + public synchronized boolean add(ProofObligation e) + { + if (!this.contains(e)) // Eliminate duplicates + { + return super.add(e); + } + + return false; + } + + @Override + public synchronized boolean addAll(Collection poList) + { + boolean changed = false; + + for (ProofObligation po: poList) + { + changed = this.add(po) || changed; + } + + return changed; + } @Override public String toString() From f5ce802439609b6ad919e54bc69148584bd6ce09 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Sun, 5 Nov 2023 15:57:21 +0000 Subject: [PATCH 2/4] Generated measure_f functions inherit pre_measure_f from pre_f. --- .../definitions/INExplicitFunctionDefinition.java | 5 ++--- .../definitions/INImplicitFunctionDefinition.java | 3 ++- .../definitions/TCExplicitFunctionDefinition.java | 13 ++++++++----- .../definitions/TCImplicitFunctionDefinition.java | 6 ++++-- 4 files changed, 16 insertions(+), 11 deletions(-) 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 a4d981046..2b466bc89 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 @@ -147,9 +147,8 @@ public NameValuePairList getNamedValues(Context ctxt) if (measureDef != null && measureDef.name.getName().startsWith("measure_")) { - FunctionValue mfunc = new FunctionValue(measureDef, null, null, null); - mfunc.uninstantiated = (typeParams != null); - nvl.add(new NameValuePair(measureDef.name, mfunc)); + // Add implicit measure_* functions and any pre_measure_*s too. + nvl.addAll(measureDef.getNamedValues(ctxt)); } return nvl; 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 2e0aed4a8..2a07b71c1 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 @@ -159,7 +159,8 @@ public NameValuePairList getNamedValues(Context ctxt) if (measureDef != null && measureDef.name.getName().startsWith("measure_")) { - nvl.add(new NameValuePair(measureDef.name, new FunctionValue(measureDef, null, null, null))); + // Add implicit measure_* functions and any pre_measure_*s too. + nvl.addAll(measureDef.getNamedValues(ctxt)); } return nvl; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCExplicitFunctionDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCExplicitFunctionDefinition.java index 6dd865607..fb9084536 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCExplicitFunctionDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCExplicitFunctionDefinition.java @@ -396,14 +396,17 @@ private void setMeasureExp(Environment base, Environment local, NameScope scope) TCPatternListList cpll = new TCPatternListList(); cpll.add(all); + // Note that the measure_f has the precondition of the function it measures. + TCExplicitFunctionDefinition def = new TCExplicitFunctionDefinition(null, accessSpecifier, measureName, - typeParams, type.getMeasureType(isCurried, actual), cpll, measureExp, null, null, false, null); + typeParams, type.getMeasureType(isCurried, actual), cpll, measureExp, precondition, null, false, null); def.classDefinition = classDefinition; + def.implicitDefinitions(base); def.typeResolve(base); + def.typeCheck(base, scope); + measureDef = def; - - measureDef.typeCheck(base, scope); } /** @@ -620,9 +623,9 @@ public TCDefinition findName(TCNameToken sought, NameScope scope) return postdef; } - if (measureDef != null && measureDef.findName(sought, scope) != null) + if (measureDef != null) { - return measureDef; + return measureDef.findName(sought, scope); // eg. pre_measure_f } return null; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCImplicitFunctionDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCImplicitFunctionDefinition.java index 888e82b3e..aaae8e29c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCImplicitFunctionDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCImplicitFunctionDefinition.java @@ -380,12 +380,14 @@ private void setMeasureExp(Environment base, Environment local, NameScope scope) measureName = name.getMeasureName(measureExp.location); checkMeasure(measureName, actual); + // Note that the measure_f has the precondition of the function it measures. + TCExplicitFunctionDefinition def = new TCExplicitFunctionDefinition(null, accessSpecifier, measureName, - typeParams, type.getMeasureType(false, actual), getParamPatternList(), measureExp, null, null, false, null); + typeParams, type.getMeasureType(false, actual), getParamPatternList(), measureExp, precondition, null, false, null); def.classDefinition = classDefinition; + def.implicitDefinitions(base); def.typeResolve(base); - def.typeCheck(base, scope); measureDef = def; From 48afd8747c7d4ef4fce7a51a41e3b4904fc582ef Mon Sep 17 00:00:00 2001 From: nick_battle Date: Sun, 5 Nov 2023 16:56:43 +0000 Subject: [PATCH 3/4] Add a maximal flag to POPatterns to allow mk_R!(...) in POs --- .../java/com/fujitsu/vdmj/po/patterns/POPattern.java | 9 +++++++++ .../com/fujitsu/vdmj/po/patterns/PORecordPattern.java | 9 ++++++++- .../com/fujitsu/vdmj/pog/TotalFunctionObligation.java | 7 ++++++- 3 files changed, 23 insertions(+), 2 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POPattern.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POPattern.java index 3e422ad8b..9a2bd1d84 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POPattern.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POPattern.java @@ -161,6 +161,15 @@ public final POPattern removeIgnorePatterns() return apply(new PORemoveIgnoresVisitor(), null); } + /** + * Indicates that the pattern is associated with a maximal type, which may + * affect the string representation - eg. mk_R!(...). + */ + public void setMaximal(boolean maximal) + { + return; // Only used in PORecordPattern + } + /** * Implemented by all patterns to allow visitor processing. */ diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/PORecordPattern.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/PORecordPattern.java index 86179cb06..a74f58afc 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/PORecordPattern.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/PORecordPattern.java @@ -35,6 +35,7 @@ public class PORecordPattern extends POPattern public final TCNameToken typename; public final POPatternList plist; public final TCType type; + private boolean maximal = false; public PORecordPattern(TCNameToken typename, POPatternList list, TCType type) { @@ -47,7 +48,7 @@ public PORecordPattern(TCNameToken typename, POPatternList list, TCType type) @Override public String toString() { - return "mk_" + type.toExplicitString(location) + "(" + Utils.listToString(plist) + ")"; + return "mk_" + type.toExplicitString(location) + (maximal ? "!(" : "(") + Utils.listToString(plist) + ")"; } @Override @@ -61,6 +62,12 @@ public boolean alwaysMatches() { return plist.alwaysMatches(); } + + @Override + public void setMaximal(boolean maximal) + { + this.maximal = maximal; + } @Override public R apply(POPatternVisitor visitor, S arg) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/TotalFunctionObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/TotalFunctionObligation.java index 2f033cf5a..b8fd86dc6 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/TotalFunctionObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/TotalFunctionObligation.java @@ -75,11 +75,16 @@ private String getContext(String name, POExplicitFunctionDefinition def) for (POPatternList pl: def.paramPatternList) { + int param = 0; + for (POPattern p: pl) { fapply.append(sep); - fapply.append(p.removeIgnorePatterns()); + POPattern p2 = p.removeIgnorePatterns(); + p2.setMaximal(ftype.parameters.get(param).isMaximal()); + fapply.append(p2); sep = ", "; + param++; } if (ftype.result instanceof TCFunctionType) From d5e133248044424748872fe50daf0a5083b5a076 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Sun, 5 Nov 2023 17:21:32 +0000 Subject: [PATCH 4/4] Treat 'not yet specified' encounter as a MAYBE --- examples/quickcheck/src/main/java/quickcheck/QuickCheck.java | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java index c7e6556fb..3fddcf226 100644 --- a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -466,6 +466,10 @@ else if (results.provedBy != null) { execResult = null; } + else if (e.number == 4024) // 'not yet specified' expression reached + { + execResult = new BooleanValue(true); // MAYBE, in effect + } else { execResult = new BooleanValue(false);