From 8bec52f6a2f3f3e105b4f95a16f8f85c966216ea Mon Sep 17 00:00:00 2001 From: nick_battle Date: Mon, 23 Oct 2023 17:02:44 +0100 Subject: [PATCH 1/4] Added null defence --- vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 d18e397d2..06a38e89d 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java @@ -95,7 +95,7 @@ public void setCounterexample(Context path) counterexample.clear(); Context ctxt = path; - while (ctxt.outer != null) + while (ctxt != null && ctxt.outer != null) { counterexample.putAll(ctxt); ctxt = ctxt.outer; From c5d5f16123ddd3285e60e706a50eaf49f8b8cd26 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Mon, 23 Oct 2023 17:03:09 +0100 Subject: [PATCH 2/4] Fix finite strategy --- .../quickcheck/strategies/FiniteQCStrategy.java | 5 +---- .../quickcheck/visitors/TrivialQCVisitor.java | 16 ++++++++++++++-- 2 files changed, 15 insertions(+), 6 deletions(-) diff --git a/examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java b/examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java index adb346b18..4f0f6a8ab 100644 --- a/examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java +++ b/examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java @@ -125,7 +125,6 @@ public Results getValues(ProofObligation po, INExpression exp, List result = new HashMap(); long before = System.currentTimeMillis(); - boolean proved = false; if (po.isCheckable) { @@ -158,11 +157,9 @@ public Results getValues(ProofObligation po, INExpression exp, List truths) public Boolean caseImpliesExpression(TCImpliesExpression node, Stack truths) { truths.push(node.left); + int pops = 1; if (node.left instanceof TCEqualsExpression) { TCEqualsExpression eq = (TCEqualsExpression)node.left; truths.push(new TCNotEqualExpression(eq.left, new LexKeywordToken(Token.NE, eq.location), eq.right)); + pops++; + } + else if (node.left instanceof TCNotExpression) + { + TCNotExpression nexp = (TCNotExpression)node.left; + + if (nexp.exp instanceof TCEqualsExpression) + { + TCEqualsExpression eq = (TCEqualsExpression)nexp.exp; + truths.push(new TCNotEqualExpression(eq.left, new LexKeywordToken(Token.NE, eq.location), eq.right)); + pops++; + } } boolean result = node.right.apply(this, truths); - if (node.left instanceof TCEqualsExpression) + for (int i=0; i Date: Mon, 23 Oct 2023 19:47:43 +0100 Subject: [PATCH 3/4] Clarify hasAllValues from finite strategy etc --- .../src/main/java/quickcheck/QuickCheck.java | 19 +++++++++++++------ .../strategies/FiniteQCStrategy.java | 10 +++++----- .../strategies/FixedQCStrategy.java | 2 +- .../strategies/RandomQCStrategy.java | 2 +- .../java/quickcheck/strategies/Results.java | 19 +++++++++++++++---- .../strategies/SearchQCStrategy.java | 2 +- .../strategies/TrivialQCStrategy.java | 9 ++++++--- .../quickcheck/example/ExampleQCStrategy.java | 9 ++++++++- 8 files changed, 50 insertions(+), 22 deletions(-) diff --git a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java index 42a9106f2..19adf1ba9 100644 --- a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -314,13 +314,14 @@ public Results getValues(ProofObligation po) if (!po.isCheckable) { - return new Results(null, union, 0); + return new Results(); } INExpression exp = getINExpression(po); List binds = getINBindList(exp); long before = System.currentTimeMillis(); IterableContext ictxt = addTypeParams(po, Interpreter.getInstance().getInitialContext()); + boolean hasAllValues = false; while (ictxt.hasNext()) { @@ -331,6 +332,11 @@ public Results getValues(ProofObligation po) Results sresults = strategy.getValues(po, exp, binds, ictxt); Map cexamples = sresults.counterexamples; + if (sresults.provedBy != null) // No need to go further + { + return new Results(sresults.provedBy, sresults.hasAllValues, cexamples, System.currentTimeMillis() - before); + } + for (String bind: cexamples.keySet()) { if (union.containsKey(bind)) @@ -343,10 +349,7 @@ public Results getValues(ProofObligation po) } } - if (sresults.provedBy != null) // No need to go further - { - return new Results(sresults.provedBy, cexamples, System.currentTimeMillis() - before); - } + hasAllValues = hasAllValues || sresults.hasAllValues; // At least one has all values } for (INBindingSetter bind: binds) @@ -361,7 +364,7 @@ public Results getValues(ProofObligation po) } } - return new Results(null, union, System.currentTimeMillis() - before); + return new Results(null, hasAllValues, union, System.currentTimeMillis() - before); } public void checkObligation(ProofObligation po, Results results) @@ -473,6 +476,10 @@ else if (result instanceof BooleanValue) { outcome = POStatus.PROVED; // An "exists" PO is PROVED, if true. } + else if (results.hasAllValues) + { + outcome = POStatus.PROVED; // All values were tested and passed, so PROVED + } else { outcome = POStatus.MAYBE; diff --git a/examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java b/examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java index 4f0f6a8ab..165cb9607 100644 --- a/examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java +++ b/examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java @@ -139,27 +139,27 @@ public Results getValues(ProofObligation po, INExpression exp, List expansionLimit) { - return new Results(null, result, 0); // Too big + return new Results(); // Too big } } catch (InternalException e) // Infinite { - return new Results(null, result, 0); + return new Results(); } catch (ArithmeticException e) // Overflow probably { - return new Results(null, result, 0); + return new Results(); } } - // Game on... + // Game on... all binds can be expanded for (INBindingSetter bind: binds) { result.put(bind.toString(), bind.getType().apply(new INGetAllValuesVisitor(), ctxt)); } } - return new Results(null, result, System.currentTimeMillis() - before); + return new Results(null, true, result, System.currentTimeMillis() - before); } @Override diff --git a/examples/quickcheck/src/main/java/quickcheck/strategies/FixedQCStrategy.java b/examples/quickcheck/src/main/java/quickcheck/strategies/FixedQCStrategy.java index 43addfd5b..597ad3a91 100644 --- a/examples/quickcheck/src/main/java/quickcheck/strategies/FixedQCStrategy.java +++ b/examples/quickcheck/src/main/java/quickcheck/strategies/FixedQCStrategy.java @@ -542,7 +542,7 @@ public Results getValues(ProofObligation po, INExpression exp, List counterexamples; - public final long duration; // time to generate counterexamples, in millisecs - - public Results(String proved, Map counterexamples, long duration) + public final long duration; // time to generate counterexamples, in millisecs + + public Results() + { + this.provedBy = null; + this.hasAllValues = false; + this.counterexamples = new HashMap(); + this.duration = 0; + } + + public Results(String proved, boolean hasAllValues, Map counterexamples, long duration) { this.provedBy = proved; + this.hasAllValues = hasAllValues; this.counterexamples = counterexamples; this.duration = duration; } diff --git a/examples/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java b/examples/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java index 24d7b4dd5..ac31c478e 100644 --- a/examples/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java +++ b/examples/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java @@ -134,7 +134,7 @@ public Results getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) { long before = System.currentTimeMillis(); - boolean proved = false; + String provedBy = null; if (po.isCheckable && po.getCheckedExpression() != null) { TrivialQCVisitor visitor = new TrivialQCVisitor(); - proved = po.getCheckedExpression().apply(visitor, new Stack()); + if (po.getCheckedExpression().apply(visitor, new Stack())) + { + provedBy = getName(); + } } - return new Results(proved ? getName() : null, new HashMap(), System.currentTimeMillis() - before); + return new Results(provedBy, false, new HashMap(), System.currentTimeMillis() - before); } @Override diff --git a/examples/quickcheck/src/test/java/quickcheck/example/ExampleQCStrategy.java b/examples/quickcheck/src/test/java/quickcheck/example/ExampleQCStrategy.java index 8f6747849..38078c194 100644 --- a/examples/quickcheck/src/test/java/quickcheck/example/ExampleQCStrategy.java +++ b/examples/quickcheck/src/test/java/quickcheck/example/ExampleQCStrategy.java @@ -104,7 +104,14 @@ public Results getValues(ProofObligation po, INExpression exp, List Date: Mon, 23 Oct 2023 20:16:54 +0100 Subject: [PATCH 4/4] Rename StrategyResults and tidy --- .../src/main/java/quickcheck/QuickCheck.java | 37 +++++++++---------- .../commands/QuickCheckCommand.java | 4 +- .../commands/QuickCheckExecutor.java | 4 +- .../strategies/FiniteQCStrategy.java | 10 ++--- .../strategies/FixedQCStrategy.java | 4 +- .../quickcheck/strategies/QCStrategy.java | 2 +- .../strategies/RandomQCStrategy.java | 4 +- .../strategies/SearchQCStrategy.java | 4 +- .../{Results.java => StrategyResults.java} | 13 ++++--- .../strategies/TrivialQCStrategy.java | 4 +- .../quickcheck/example/ExampleQCStrategy.java | 8 ++-- 11 files changed, 48 insertions(+), 46 deletions(-) rename examples/quickcheck/src/main/java/quickcheck/strategies/{Results.java => StrategyResults.java} (79%) diff --git a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java index 19adf1ba9..4abc5bc97 100644 --- a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -70,7 +70,7 @@ import annotations.IterableContext; import annotations.po.POQuickCheckAnnotation; import quickcheck.strategies.QCStrategy; -import quickcheck.strategies.Results; +import quickcheck.strategies.StrategyResults; import quickcheck.visitors.FixedRangeCreator; import quickcheck.visitors.TypeBindFinder; @@ -308,13 +308,13 @@ public List getINBindList(INExpression inexp) return inexp.apply(new TypeBindFinder(), null); } - public Results getValues(ProofObligation po) + public StrategyResults getValues(ProofObligation po) { Map union = new HashMap(); if (!po.isCheckable) { - return new Results(); + return new StrategyResults(); } INExpression exp = getINExpression(po); @@ -329,12 +329,12 @@ public Results getValues(ProofObligation po) for (QCStrategy strategy: strategies) { - Results sresults = strategy.getValues(po, exp, binds, ictxt); + StrategyResults sresults = strategy.getValues(po, exp, binds, ictxt); Map cexamples = sresults.counterexamples; if (sresults.provedBy != null) // No need to go further { - return new Results(sresults.provedBy, sresults.hasAllValues, cexamples, System.currentTimeMillis() - before); + return new StrategyResults(sresults.provedBy, sresults.hasAllValues, cexamples, System.currentTimeMillis() - before); } for (String bind: cexamples.keySet()) @@ -364,10 +364,10 @@ public Results getValues(ProofObligation po) } } - return new Results(null, hasAllValues, union, System.currentTimeMillis() - before); + return new StrategyResults(null, hasAllValues, union, System.currentTimeMillis() - before); } - public void checkObligation(ProofObligation po, Results results) + public void checkObligation(ProofObligation po, StrategyResults results) { try { @@ -413,9 +413,6 @@ else if (results.provedBy != null) } } - long before = System.currentTimeMillis(); - Value result = new BooleanValue(false); - ContextException exception = null; Context ctxt = Interpreter.getInstance().getInitialContext(); if (Settings.dialect != Dialect.VDM_SL) @@ -432,6 +429,9 @@ else if (results.provedBy != null) } IterableContext ictxt = addTypeParams(po, ctxt); + Value execResult = new BooleanValue(false); + ContextException exception = null; + long before = System.currentTimeMillis(); try { @@ -440,35 +440,35 @@ else if (results.provedBy != null) do { ictxt.next(); - result = poexp.eval(ictxt); + execResult = poexp.eval(ictxt); } - while (ictxt.hasNext() && result.boolValue(ctxt)); + while (ictxt.hasNext() && execResult.boolValue(ctxt)); } catch (ContextException e) { if (e.rawMessage.equals("Execution cancelled")) { - result = null; + execResult = null; } else { - result = new BooleanValue(false); + execResult = new BooleanValue(false); exception = e; } } long after = System.currentTimeMillis() + results.duration; - if (result == null) // cancelled + if (execResult == null) // cancelled { println("----"); printBindings(bindings); println("----"); println(po); } - else if (result instanceof BooleanValue) + else if (execResult instanceof BooleanValue) { - if (result.boolValue(ctxt)) + if (execResult.boolValue(ctxt)) { POStatus outcome = null; @@ -515,7 +515,7 @@ else if (results.hasAllValues) } else { - String msg = String.format("Error: PO evaluation returns %s?\n", result.kind()); + String msg = String.format("Error: PO evaluation returns %s?\n", execResult.kind()); printf("PO #%d, %s\n", po.number, msg); po.setStatus(POStatus.FAILED); po.setCounterMessage(msg); @@ -550,7 +550,6 @@ else if (results.hasAllValues) { errorCount++; println(e); - return; } } diff --git a/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java b/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java index 15244d0e1..d462a64c4 100644 --- a/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java +++ b/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java @@ -40,7 +40,7 @@ import quickcheck.QuickCheck; import quickcheck.strategies.QCStrategy; -import quickcheck.strategies.Results; +import quickcheck.strategies.StrategyResults; public class QuickCheckCommand extends AnalysisCommand { @@ -141,7 +141,7 @@ public String run(String line) { for (ProofObligation po: chosen) { - Results results = qc.getValues(po); + StrategyResults results = qc.getValues(po); if (!qc.hasErrors()) { diff --git a/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckExecutor.java b/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckExecutor.java index 71e022982..27b18b6e3 100644 --- a/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckExecutor.java +++ b/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckExecutor.java @@ -36,7 +36,7 @@ import json.JSONObject; import lsp.LSPServer; import quickcheck.QuickCheck; -import quickcheck.strategies.Results; +import quickcheck.strategies.StrategyResults; import rpc.RPCRequest; import workspace.PluginRegistry; import workspace.plugins.POPlugin; @@ -77,7 +77,7 @@ protected void exec() throws Exception { for (ProofObligation po: chosen) { - Results results = qc.getValues(po); + StrategyResults results = qc.getValues(po); if (!qc.hasErrors()) { diff --git a/examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java b/examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java index 165cb9607..718ea7a59 100644 --- a/examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java +++ b/examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java @@ -121,7 +121,7 @@ public boolean init(QuickCheck qc) } @Override - public Results getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) + public StrategyResults getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) { HashMap result = new HashMap(); long before = System.currentTimeMillis(); @@ -139,16 +139,16 @@ public Results getValues(ProofObligation po, INExpression exp, List expansionLimit) { - return new Results(); // Too big + return new StrategyResults(); // Too big } } catch (InternalException e) // Infinite { - return new Results(); + return new StrategyResults(); } catch (ArithmeticException e) // Overflow probably { - return new Results(); + return new StrategyResults(); } } @@ -159,7 +159,7 @@ public Results getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) + public StrategyResults getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) { Map values = new HashMap(); long before = System.currentTimeMillis(); @@ -542,7 +542,7 @@ public Results getValues(ProofObligation po, INExpression exp, List binds, Context ctxt); + abstract public StrategyResults getValues(ProofObligation po, INExpression exp, List binds, Context ctxt); abstract public String help(); } diff --git a/examples/quickcheck/src/main/java/quickcheck/strategies/RandomQCStrategy.java b/examples/quickcheck/src/main/java/quickcheck/strategies/RandomQCStrategy.java index 679047cf3..493aa3a48 100644 --- a/examples/quickcheck/src/main/java/quickcheck/strategies/RandomQCStrategy.java +++ b/examples/quickcheck/src/main/java/quickcheck/strategies/RandomQCStrategy.java @@ -127,7 +127,7 @@ public boolean init(QuickCheck qc) } @Override - public Results getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) + public StrategyResults getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) { HashMap result = new HashMap(); long before = System.currentTimeMillis(); @@ -144,7 +144,7 @@ public Results getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) + public StrategyResults getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) { HashMap result = new HashMap(); long before = System.currentTimeMillis(); @@ -134,7 +134,7 @@ public Results getValues(ProofObligation po, INExpression exp, List counterexamples; public final long duration; // time to generate counterexamples, in millisecs - public Results() + public StrategyResults() { this.provedBy = null; this.hasAllValues = false; @@ -49,7 +52,7 @@ public Results() this.duration = 0; } - public Results(String proved, boolean hasAllValues, Map counterexamples, long duration) + public StrategyResults(String proved, boolean hasAllValues, Map counterexamples, long duration) { this.provedBy = proved; this.hasAllValues = hasAllValues; diff --git a/examples/quickcheck/src/main/java/quickcheck/strategies/TrivialQCStrategy.java b/examples/quickcheck/src/main/java/quickcheck/strategies/TrivialQCStrategy.java index 0f2f3256f..3d982e830 100644 --- a/examples/quickcheck/src/main/java/quickcheck/strategies/TrivialQCStrategy.java +++ b/examples/quickcheck/src/main/java/quickcheck/strategies/TrivialQCStrategy.java @@ -79,7 +79,7 @@ public boolean init(QuickCheck qc) } @Override - public Results getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) + public StrategyResults getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) { long before = System.currentTimeMillis(); String provedBy = null; @@ -93,7 +93,7 @@ public Results getValues(ProofObligation po, INExpression exp, List(), System.currentTimeMillis() - before); + return new StrategyResults(provedBy, false, new HashMap(), System.currentTimeMillis() - before); } @Override diff --git a/examples/quickcheck/src/test/java/quickcheck/example/ExampleQCStrategy.java b/examples/quickcheck/src/test/java/quickcheck/example/ExampleQCStrategy.java index 38078c194..ed89f93df 100644 --- a/examples/quickcheck/src/test/java/quickcheck/example/ExampleQCStrategy.java +++ b/examples/quickcheck/src/test/java/quickcheck/example/ExampleQCStrategy.java @@ -38,7 +38,7 @@ import quickcheck.QuickCheck; import quickcheck.strategies.QCStrategy; -import quickcheck.strategies.Results; +import quickcheck.strategies.StrategyResults; public class ExampleQCStrategy extends QCStrategy { @@ -94,7 +94,7 @@ public boolean init(QuickCheck qc) } @Override - public Results getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) + public StrategyResults getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) { Map values = new HashMap(); long before = System.currentTimeMillis(); @@ -106,11 +106,11 @@ public Results getValues(ProofObligation po, INExpression exp, List