From 36c8336cffeda2e1ea5b8f7840f8e7d3f8e43b4a Mon Sep 17 00:00:00 2001 From: Valentin Date: Mon, 21 Feb 2022 12:08:57 +0100 Subject: [PATCH 1/5] QuantifierInstantiation is a FocusProofRule. In particular, it is not a NoFocusProofRule. --- .../iti/algover/rules/NoFocusProofRule.java | 1 + .../rules/impl/QuantifierInstantiation.java | 18 +-- modules/fxgui/ListExample/AlgoVerList.dfy | 2 +- .../fxgui/ListExample/AlgoVerList.dfy.proofs | 117 ++++++++++++++++-- .../rule/RuleApplicationController.java | 1 + .../kit/iti/algover/rule/RuleViewOverlay.java | 5 +- 6 files changed, 113 insertions(+), 31 deletions(-) diff --git a/modules/core/src/edu/kit/iti/algover/rules/NoFocusProofRule.java b/modules/core/src/edu/kit/iti/algover/rules/NoFocusProofRule.java index 12c4e3661..211d4ae05 100644 --- a/modules/core/src/edu/kit/iti/algover/rules/NoFocusProofRule.java +++ b/modules/core/src/edu/kit/iti/algover/rules/NoFocusProofRule.java @@ -29,6 +29,7 @@ public final ProofRuleApplication considerApplication(ProofNode target, Sequent try { Parameters params = new Parameters(); + ProofRuleApplication result = makeApplication(target, params); return result; } catch (NotApplicableException e) { diff --git a/modules/core/src/edu/kit/iti/algover/rules/impl/QuantifierInstantiation.java b/modules/core/src/edu/kit/iti/algover/rules/impl/QuantifierInstantiation.java index 4ca3bbf65..2f1ef7dcd 100644 --- a/modules/core/src/edu/kit/iti/algover/rules/impl/QuantifierInstantiation.java +++ b/modules/core/src/edu/kit/iti/algover/rules/impl/QuantifierInstantiation.java @@ -8,18 +8,8 @@ import de.uka.ilkd.pp.NoExceptions; import edu.kit.iti.algover.proof.ProofFormula; import edu.kit.iti.algover.proof.ProofNode; -import edu.kit.iti.algover.rules.DefaultFocusProofRule; -import edu.kit.iti.algover.rules.NoFocusProofRule; -import edu.kit.iti.algover.rules.NotApplicableException; -import edu.kit.iti.algover.rules.ParameterDescription; -import edu.kit.iti.algover.rules.ParameterType; -import edu.kit.iti.algover.rules.Parameters; -import edu.kit.iti.algover.rules.ProofRuleApplication; +import edu.kit.iti.algover.rules.*; import edu.kit.iti.algover.rules.ProofRuleApplication.Applicability; -import edu.kit.iti.algover.rules.ProofRuleApplicationBuilder; -import edu.kit.iti.algover.rules.RuleException; -import edu.kit.iti.algover.rules.TermParameter; -import edu.kit.iti.algover.rules.TermSelector; import edu.kit.iti.algover.rules.TermSelector.SequentPolarity; import edu.kit.iti.algover.term.ApplTerm; import edu.kit.iti.algover.term.DefaultTermVisitor; @@ -36,7 +26,7 @@ /** * Created by jklamroth on 10/25/18. */ -public class QuantifierInstantiation extends NoFocusProofRule { +public class QuantifierInstantiation extends FocusProofRule { public static final ParameterDescription WITH_PARAM = new ParameterDescription<>("with", ParameterType.TERM, true); @@ -45,7 +35,7 @@ public class QuantifierInstantiation extends NoFocusProofRule { new ParameterDescription<>("var", ParameterType.STRING, false); public QuantifierInstantiation() { - super(DefaultFocusProofRule.ON_PARAM_OPT, WITH_PARAM); + super(ON_PARAM_REQ, WITH_PARAM); } @Override @@ -56,7 +46,7 @@ public String getName() { @Override protected ProofRuleApplication makeApplicationImpl(ProofNode target, Parameters parameters) throws RuleException { - TermParameter onParam = parameters.getValue(DefaultFocusProofRule.ON_PARAM_OPT); + TermParameter onParam = parameters.getValue(ON_PARAM_REQ); TermParameter withParam = parameters.getValue(WITH_PARAM); if(onParam == null) { diff --git a/modules/fxgui/ListExample/AlgoVerList.dfy b/modules/fxgui/ListExample/AlgoVerList.dfy index 33bf5a9dc..8b499e2f1 100644 --- a/modules/fxgui/ListExample/AlgoVerList.dfy +++ b/modules/fxgui/ListExample/AlgoVerList.dfy @@ -51,7 +51,7 @@ class List { //currently inserting at position 0 is not supported (but should be an easy extension) method insertAt(pos: int, value: int) requires 0 <= pos < |seqq| && Valid() - ensures seqq == old(seqq[..pos] + [value] + seqq[pos..]) + ensures seqq == old(seqq[..pos]) + [value] + old(seqq[pos..]) ensures Valid() modifies footprint { diff --git a/modules/fxgui/ListExample/AlgoVerList.dfy.proofs b/modules/fxgui/ListExample/AlgoVerList.dfy.proofs index 8ea0245dd..903f4f58b 100644 --- a/modules/fxgui/ListExample/AlgoVerList.dfy.proofs +++ b/modules/fxgui/ListExample/AlgoVerList.dfy.proofs @@ -1,7 +1,7 @@ -Created by DIVE at Thu Apr 01 09:05:25 CEST 2021 +Created by DIVE at Fri Feb 18 19:13:53 CET 2022 boogie; boogie; boogie; @@ -12,18 +12,111 @@ boogie; boogie; boogie; -skip; -expand on='_ |-'; -vsasad -expand on='_ |-'; -skip;fwef - +boogie; +boogie; boogie; boogie; boogie; boogie; boogie; - +substitute on='|- _';substitute on='|- _';substitute on='|- _';substitute on='|- _';substitute on='|- _';andRight on='|- _';cases { + "case 1": + boogie; + "case 2": + skip; + substitute on='let node := node₁ :: _'; + substitute on='let idx := idx₁ :: node₁ == this.nodeseqq[idx]'; + substitute on='let idx := idx₁ :: idx <= pos && idx >= 0'; + substitute on='let idx := idx₁ :: _'; + substitute on='let this, value, next := + $new₁ + , value + , (node₁.next@($heap[$create($new₁)])) :: _'; + andLeft on='0 <= pos && pos < |this.seqq| && this.Valid()'; + andLeft on='0 <= pos && pos < |this.seqq|'; + andLeft on='_ && _'; + expand on='this.Valid()'; + prop; + skip; + inst on=A.10 with='pos'; + inst on=A.11 with='pos'; + inst on=A.12 with='pos'; + inst on=A.15 with='pos'; + skip; + impLeft on='pos >= 0 && pos < |this.nodeseqq| ==> this.nodeseqq[pos] != null'; + cases { + "mainBranch": + impLeft on='pos >= 0 && pos < |this.nodeseqq| - 1 ==> this.nodeseqq[pos].next != null'; + cases { + "mainBranch": + impLeft on='pos >= 0 && pos < |this.seqq| ==> this.seqq[pos] == this.nodeseqq[pos].value'; + cases { + "mainBranch": + impLeft on='_ ==> _'; + cases { + "mainBranch": + notLeft on='!(idx₁ < pos)'; + skip; + notLeft on='!$isCreated($heap, $new₁)'; + skip; + "": + boogie; + } + "": + boogie; + } + "": + notLeft on='!(pos >= 0 && pos < |this.nodeseqq| - 1)'; + andRight on='|- _ && _'; + cases { + "case 1": + z3; + "case 2": + impLeft on='pos >= 0 && pos < |this.nodeseqq| - 1 ==> this.nodeseqq[pos].next == this.nodeseqq[(pos + 1)]'; + cases { + "mainBranch": + notLeft on='!(idx₁ < pos)'; + prop; + cases { + "case 1": + z3; + "case 2": + boogie; + "case 3": + skip; + } + "": + prop; + cases { + "case 1": + skip; + z3; + "case 2": + "case 3": + skip; + notLeft on='!(pos >= 0 && pos < |this.nodeseqq| - 1)'; + andRight on='_ && _'; + cases { + "case 1": + z3; + "case 2": + notLeft on='!(idx₁ < pos)'; + } + } + } + } + } + "": + notLeft on='!(pos >= 0 && pos < |this.nodeseqq|)'; + andRight on='|- _ && _'; + cases { + "case 1": + z3; + "case 2": + boogie; + } + } +} boogie; boogie; boogie; @@ -45,7 +138,7 @@ skip;fwef boogie; boogie; boogie; -expand on='_.Valid()@_'; +boogie; boogie; boogie; boogie; @@ -89,11 +182,11 @@ skip;fwef boogie; boogie; -expand on='_.Valid()@_'; +boogie; boogie; boogie; boogie; -skip;skip;skip;skip;expand on='_ |-';prop;skip;boogie; +expand on='_ |-';prop;skip;substitute on='|- _';close on='|- _'; boogie; boogie; boogie; @@ -102,6 +195,6 @@ skip;fwef boogie; - +substitute on='let node := node₁ :: _ |-';substitute on='let idx := idx₁ :: node₁ == this.nodeseqq[idx]';substitute on='let idx := idx₁ :: idx <= pos && idx >= 0';substitute on='let idx := idx₁ :: _';substitute on=S.0.0.0.0.0.0.0.0.0.1.0.0;substitute on=S.0.0.0.0.0.0.0.0.0.1.1;substitute on='|- _';substitute on='|- _';substitute on='|- _';substitute on='|- _';skip;substitute on=S.0.1.1;skip;substitute on='|- _';substitute on='|- _';substitute on='|- _';substitute on='|- _';prop;skip;expand on='this.Valid()';prop;skip; boogie; diff --git a/modules/fxgui/src/edu/kit/iti/algover/rule/RuleApplicationController.java b/modules/fxgui/src/edu/kit/iti/algover/rule/RuleApplicationController.java index e0e4adde3..1f6d18b07 100644 --- a/modules/fxgui/src/edu/kit/iti/algover/rule/RuleApplicationController.java +++ b/modules/fxgui/src/edu/kit/iti/algover/rule/RuleApplicationController.java @@ -241,6 +241,7 @@ public void addProofRule(ProofRule rule) { public void considerApplication(ProofNode target, Sequent selection, TermSelector selector) { if(target != null) { + // isValidForSequent could be avoided if selector is properly reset on proofchange if (selector != null && selector.isValidForSequent(selection)) { try { Term term = selector.selectSubterm(selection); diff --git a/modules/fxgui/src/edu/kit/iti/algover/rule/RuleViewOverlay.java b/modules/fxgui/src/edu/kit/iti/algover/rule/RuleViewOverlay.java index f2473aa23..d1467e040 100644 --- a/modules/fxgui/src/edu/kit/iti/algover/rule/RuleViewOverlay.java +++ b/modules/fxgui/src/edu/kit/iti/algover/rule/RuleViewOverlay.java @@ -95,10 +95,7 @@ private void onRuleApplication(MouseEvent mouseEvent) { requiredParams++; } } - if (mouseEvent.isShiftDown() || (requiredParams > 0 && - (application.getRule().getAllParameters().size() == 1 && - (!application.getRule().getAllParameters().containsValue(FocusProofRule.ON_PARAM_REQ) && - !application.getRule().getAllParameters().containsValue(DefaultFocusProofRule.ON_PARAM_OPT))))) { + if (mouseEvent.isShiftDown() || requiredParams > 0) { String on; try { PrettyPrint pp = new PrettyPrint(); From 98c038b79c26cb8b1f598def994139de432b57eb Mon Sep 17 00:00:00 2001 From: Valentin Date: Wed, 23 Feb 2022 23:38:58 +0100 Subject: [PATCH 2/5] Query required params on rule application. --- modules/core/src/edu/kit/iti/algover/rules/Parameters.java | 4 ++-- .../fxgui/src/edu/kit/iti/algover/rule/RuleViewOverlay.java | 6 ++++-- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/modules/core/src/edu/kit/iti/algover/rules/Parameters.java b/modules/core/src/edu/kit/iti/algover/rules/Parameters.java index a0f1b0778..b9b4b8d9e 100644 --- a/modules/core/src/edu/kit/iti/algover/rules/Parameters.java +++ b/modules/core/src/edu/kit/iti/algover/rules/Parameters.java @@ -87,8 +87,8 @@ public boolean hasValue(@NonNull ParameterDescription param) { * via {@link ParameterDescription#getName()}. * * @param param the parameter description to look up. - * @return the value stored for that variable, null if no such - * value + * @return the value stored for that variable, {@link ParameterDescription#getDefaultValue()}, if value not + * explicitly specified, null if no such value. * @throws ClassCastException if the value is not assign-compatible with the * type in the parameter description. */ diff --git a/modules/fxgui/src/edu/kit/iti/algover/rule/RuleViewOverlay.java b/modules/fxgui/src/edu/kit/iti/algover/rule/RuleViewOverlay.java index d1467e040..58fb66d19 100644 --- a/modules/fxgui/src/edu/kit/iti/algover/rule/RuleViewOverlay.java +++ b/modules/fxgui/src/edu/kit/iti/algover/rule/RuleViewOverlay.java @@ -90,12 +90,14 @@ public RuleViewOverlay(ProofRuleApplication application, RuleApplicationListener private void onRuleApplication(MouseEvent mouseEvent) { int requiredParams = 0; + + for(ParameterDescription p : application.getRule().getAllParameters().values()) { - if(p.isRequired() && p.getDefaultValue().isEmpty()) { + if(p.isRequired() && application.getParameters().getValue(p) == null) { requiredParams++; } } - if (mouseEvent.isShiftDown() || requiredParams > 0) { + if (mouseEvent.isShiftDown() || (requiredParams > 0 )) { String on; try { PrettyPrint pp = new PrettyPrint(); From 8dc042ef3665aca6005af0085d86d41d85f28403 Mon Sep 17 00:00:00 2001 From: Valentin Date: Mon, 7 Mar 2022 14:01:02 +0100 Subject: [PATCH 3/5] Bugfix for heap updates on LetSubstitution. Including inlineLet in Expansion rule. --- .../impl/FunctionDefinitionExpansionRule.java | 24 ++++++++++++++++--- .../rules/impl/SubstitutionVisitor.java | 17 +++++++++---- .../edu/kit/iti/algover/MainController.java | 22 ++++++++++------- .../rule/RuleApplicationController.java | 4 ++-- 4 files changed, 50 insertions(+), 17 deletions(-) diff --git a/modules/core/src/edu/kit/iti/algover/rules/impl/FunctionDefinitionExpansionRule.java b/modules/core/src/edu/kit/iti/algover/rules/impl/FunctionDefinitionExpansionRule.java index 56dd935df..466252c95 100644 --- a/modules/core/src/edu/kit/iti/algover/rules/impl/FunctionDefinitionExpansionRule.java +++ b/modules/core/src/edu/kit/iti/algover/rules/impl/FunctionDefinitionExpansionRule.java @@ -33,6 +33,7 @@ import edu.kit.iti.algover.util.Util; import java.util.*; +import java.util.stream.Collectors; /** * This proof rule allows one to expand an application of a function symbol to @@ -244,12 +245,29 @@ private static Term instantiate(Term call, DafnyFunction function, DafnyTree tre } Term translation = ttt.build(tree); - translation = new LetTerm(assignments, translation); + LetTerm letTranslation = new LetTerm(assignments, translation); + /** + * Use {@link SubstitutionVisitor} that introduces bugfix for heap updates. + */ if(inline) { - translation = LetInlineVisitor.inline(translation); + Map substitutionMap = + letTranslation.getSubstitutions() + .stream() + .collect(Collectors.toMap(pair -> pair.fst.getName(), pair -> pair.snd)); + + Term inner = letTranslation.getTerm(0); + try { + Term result = inner.accept(new SubstitutionVisitor(), substitutionMap); + result = AlphaNormalisation.normalise(result); + + return result; + } + catch(RuleException re) { + re.printStackTrace(); + } } - return translation; + return letTranslation; } diff --git a/modules/core/src/edu/kit/iti/algover/rules/impl/SubstitutionVisitor.java b/modules/core/src/edu/kit/iti/algover/rules/impl/SubstitutionVisitor.java index acb40faad..87e0be713 100644 --- a/modules/core/src/edu/kit/iti/algover/rules/impl/SubstitutionVisitor.java +++ b/modules/core/src/edu/kit/iti/algover/rules/impl/SubstitutionVisitor.java @@ -38,6 +38,7 @@ public class SubstitutionVisitor implements TermVisitor, Term, /** * Variables get substituted, when they have something to be substituted in the * substitution table "substitutions". + * TODO: unless they are being shadowed. */ @Override public Term visit(VariableTerm variableTerm, Map substitutions) throws RuleException { @@ -101,10 +102,18 @@ public Term visit(ApplTerm applTerm, Map substitutions) throws Rul Term inner = applTerm.getTerm(i); Term innerReplaced = inner.accept(this, substitutions); subterms[i] = innerReplaced; - - anythingNew |= inner != innerReplaced; // So that we know, when we cannot preserve identity anymore + anythingNew |= !inner.equals(innerReplaced); // So that we know, when we cannot preserve identity anymore } if (!anythingNew) { + // $heap() is a ApplTerm. Updates are handled by substitution. I. e., heap() is + // substituted by Store(heap,...). If the heap is updated a substition of the for + // "heap" -> .. is in the substitutions map. + // So this is a quick fix (tests pass) + if (subterms.length == 0) { + Term sub = substitutions.get(applTerm.getSort().getName()); + if (sub != null) + return sub; + } return applTerm; } else { try { @@ -129,11 +138,11 @@ public Term visit(LetTerm letTerm, Map substitutions) throws RuleE VariableTerm var = pair.fst; Term letSubst = pair.snd; // No need to shadow yet. - // (Valentin) Why not? Term letSubstChanged = letSubst.accept(this, substitutions); + substitutedLetSubstitutions.add(new Pair<>(var, letSubstChanged)); - substitutionsChanged |= letSubst != letSubstChanged; + substitutionsChanged |= !letSubst.equals(letSubstChanged); } // Substitute the inner of the let diff --git a/modules/fxgui/src/edu/kit/iti/algover/MainController.java b/modules/fxgui/src/edu/kit/iti/algover/MainController.java index d16503bd0..46d2f146e 100644 --- a/modules/fxgui/src/edu/kit/iti/algover/MainController.java +++ b/modules/fxgui/src/edu/kit/iti/algover/MainController.java @@ -650,14 +650,20 @@ public void onRuleApplication(ProofRuleApplication application) { @Override public void onScriptSave() { - String pvcIdentifier = PropertyManager.getInstance().currentProof.get().getPVC().getIdentifier(); - try { - //manager.saveProofScriptForPVC(pvcIdentifier, PropertyManager.getInstance().currentProof.get()); - manager.saveProofScripts(); - Logger.getLogger(Logger.GLOBAL_LOGGER_NAME).info("Successfully saved script " + pvcIdentifier + "."); - } catch (IOException e) { - Logger.getLogger(Logger.GLOBAL_LOGGER_NAME).severe("Error saving script."); - e.printStackTrace(); + Proof curP = PropertyManager.getInstance().currentProof.get(); + String pvcIdentifier = ""; + if (curP != null) { + pvcIdentifier = curP.getPVC().getIdentifier(); + try { + //manager.saveProofScriptForPVC(pvcIdentifier, PropertyManager.getInstance().currentProof.get()); + manager.saveProofScripts(); + Logger.getLogger(Logger.GLOBAL_LOGGER_NAME).info("Successfully saved script " + pvcIdentifier + "."); + } catch (IOException e) { + Logger.getLogger(Logger.GLOBAL_LOGGER_NAME).severe("Error saving script."); + e.printStackTrace(); + } + } else { + Logger.getLogger(Logger.GLOBAL_LOGGER_NAME).info("No PVC selected."); } } diff --git a/modules/fxgui/src/edu/kit/iti/algover/rule/RuleApplicationController.java b/modules/fxgui/src/edu/kit/iti/algover/rule/RuleApplicationController.java index 1f6d18b07..709966a4c 100644 --- a/modules/fxgui/src/edu/kit/iti/algover/rule/RuleApplicationController.java +++ b/modules/fxgui/src/edu/kit/iti/algover/rule/RuleApplicationController.java @@ -156,7 +156,7 @@ public RuleApplicationController(ExecutorService executor, RuleApplicationListen })); - scriptRepText.getView().textProperty().addListener((observable, oldValue, newValue) -> { + /*scriptRepText.getView().textProperty().addListener((observable, oldValue, newValue) -> { String pvcIdentifier = PropertyManager.getInstance().currentProof.get().getPVC().getIdentifier(); String inFile = ""; try { @@ -168,7 +168,7 @@ public RuleApplicationController(ExecutorService executor, RuleApplicationListen inFile = inFile.replaceAll("[\\n\\t ]", ""); String textFieldReference = newValue.replaceAll("[\\n\\t ]", ""); lbUnsavedScript.setVisible(!inFile.equals(textFieldReference)); - }); + });*/ PropertyManager.getInstance().currentlyDisplayedView.addListener((observable, oldValue, newValue) -> { if (newValue.intValue() == TimelineFactory.DefaultViewPosition.SEQUENT_RULE.index) { From c2b05190a6814248f99e7bb71b4dfd57856600c0 Mon Sep 17 00:00:00 2001 From: Valentin Date: Mon, 7 Mar 2022 14:01:39 +0100 Subject: [PATCH 4/5] removed TODO --- .../src/edu/kit/iti/algover/rules/impl/SubstitutionVisitor.java | 1 - 1 file changed, 1 deletion(-) diff --git a/modules/core/src/edu/kit/iti/algover/rules/impl/SubstitutionVisitor.java b/modules/core/src/edu/kit/iti/algover/rules/impl/SubstitutionVisitor.java index 87e0be713..aac78b822 100644 --- a/modules/core/src/edu/kit/iti/algover/rules/impl/SubstitutionVisitor.java +++ b/modules/core/src/edu/kit/iti/algover/rules/impl/SubstitutionVisitor.java @@ -38,7 +38,6 @@ public class SubstitutionVisitor implements TermVisitor, Term, /** * Variables get substituted, when they have something to be substituted in the * substitution table "substitutions". - * TODO: unless they are being shadowed. */ @Override public Term visit(VariableTerm variableTerm, Map substitutions) throws RuleException { From 42f59dea7e144710e6c1b4189e7ddfe0a5a7d3d1 Mon Sep 17 00:00:00 2001 From: Valentin Date: Wed, 9 Mar 2022 11:00:38 +0100 Subject: [PATCH 5/5] remove duplicate class Node from example. --- modules/fxgui/ListExample/AlgoVerList.dfy | 26 ++-- .../fxgui/ListExample/AlgoVerList.dfy.proofs | 147 ++++++------------ 2 files changed, 56 insertions(+), 117 deletions(-) diff --git a/modules/fxgui/ListExample/AlgoVerList.dfy b/modules/fxgui/ListExample/AlgoVerList.dfy index 8b499e2f1..794587bb5 100644 --- a/modules/fxgui/ListExample/AlgoVerList.dfy +++ b/modules/fxgui/ListExample/AlgoVerList.dfy @@ -1,3 +1,11 @@ +// ---- Automatically generated settings ---- +//> settings { +//> "KeY Timeout" = "10", +//> "Dafny Timeout" = "5", +//> "SMT Timeout" = "10", +//> "Sequent Generation Type" = "inline" +//> } +// ---- End of settings ---- class Node { var value: int @@ -15,9 +23,12 @@ class List { ghost var seqq: seq; ghost var nodeseqq: seq; ghost var footprint: set; + var head: Node; + function Valid() : bool + reads this { |seqq| == |nodeseqq| && |seqq| >= 1 && @@ -65,8 +76,7 @@ class List { node := node.next; idx := idx + 1; } - var newNode := new Node; - newNode.Init(value, node.next); + var newNode := new Node.Init(value, node.next); node.next := newNode; nodeseqq := nodeseqq[..pos] + [newNode] + nodeseqq[pos..]; seqq := seqq[..pos] + [value] + seqq[pos..]; @@ -121,15 +131,3 @@ class List { v := node.value; } } - -class Node { - var value: int - var next: Node - - method Init(value: int, next : Node) - modifies this; - { - this.value := value; - this.next := next; - } -} \ No newline at end of file diff --git a/modules/fxgui/ListExample/AlgoVerList.dfy.proofs b/modules/fxgui/ListExample/AlgoVerList.dfy.proofs index 903f4f58b..8e6777e84 100644 --- a/modules/fxgui/ListExample/AlgoVerList.dfy.proofs +++ b/modules/fxgui/ListExample/AlgoVerList.dfy.proofs @@ -1,7 +1,7 @@ -Created by DIVE at Fri Feb 18 19:13:53 CET 2022 +Created by DIVE at Tue Mar 08 09:27:04 CET 2022 boogie; boogie; boogie; @@ -19,101 +19,34 @@ boogie; boogie; boogie; -substitute on='|- _';substitute on='|- _';substitute on='|- _';substitute on='|- _';substitute on='|- _';andRight on='|- _';cases { +andRight on='|- _';cases { "case 1": - boogie; + z3; "case 2": + notLeft on='!$isCreated($heap, $new₁)'; + notLeft on='!_'; + prop; skip; - substitute on='let node := node₁ :: _'; - substitute on='let idx := idx₁ :: node₁ == this.nodeseqq[idx]'; - substitute on='let idx := idx₁ :: idx <= pos && idx >= 0'; - substitute on='let idx := idx₁ :: _'; - substitute on='let this, value, next := - $new₁ - , value - , (node₁.next@($heap[$create($new₁)])) :: _'; - andLeft on='0 <= pos && pos < |this.seqq| && this.Valid()'; - andLeft on='0 <= pos && pos < |this.seqq|'; - andLeft on='_ && _'; expand on='this.Valid()'; prop; skip; - inst on=A.10 with='pos'; - inst on=A.11 with='pos'; - inst on=A.12 with='pos'; - inst on=A.15 with='pos'; - skip; - impLeft on='pos >= 0 && pos < |this.nodeseqq| ==> this.nodeseqq[pos] != null'; + inst on='(forall j:int :: j >= 0 && j < |this.nodeseqq| - 1 ==> this.nodeseqq[j].next == this.nodeseqq[(j + 1)])' with='idx₁'; + impLeft on='_ ==> _ |-'; cases { "mainBranch": - impLeft on='pos >= 0 && pos < |this.nodeseqq| - 1 ==> this.nodeseqq[pos].next != null'; + inst on='(forall n:int :: n >= 0 && n < |this.nodeseqq| ==> this.nodeseqq[n] != null)' with='pos'; + impLeft on='_ ==> _ |-'; cases { "mainBranch": - impLeft on='pos >= 0 && pos < |this.seqq| ==> this.seqq[pos] == this.nodeseqq[pos].value'; - cases { - "mainBranch": - impLeft on='_ ==> _'; - cases { - "mainBranch": - notLeft on='!(idx₁ < pos)'; - skip; - notLeft on='!$isCreated($heap, $new₁)'; - skip; - "": - boogie; - } - "": - boogie; - } "": - notLeft on='!(pos >= 0 && pos < |this.nodeseqq| - 1)'; - andRight on='|- _ && _'; - cases { - "case 1": - z3; - "case 2": - impLeft on='pos >= 0 && pos < |this.nodeseqq| - 1 ==> this.nodeseqq[pos].next == this.nodeseqq[(pos + 1)]'; - cases { - "mainBranch": - notLeft on='!(idx₁ < pos)'; - prop; - cases { - "case 1": - z3; - "case 2": - boogie; - "case 3": - skip; - } - "": - prop; - cases { - "case 1": - skip; - z3; - "case 2": - "case 3": - skip; - notLeft on='!(pos >= 0 && pos < |this.nodeseqq| - 1)'; - andRight on='_ && _'; - cases { - "case 1": - z3; - "case 2": - notLeft on='!(idx₁ < pos)'; - } - } - } - } } "": - notLeft on='!(pos >= 0 && pos < |this.nodeseqq|)'; + notLeft on='!(idx₁ >= 0 && idx₁ < |this.nodeseqq| - 1)'; andRight on='|- _ && _'; cases { "case 1": z3; "case 2": - boogie; } } } @@ -146,39 +79,47 @@ boogie; boogie; - - +andRight on='|- _';cases { + "case 1": + z3; + "case 2": +} +andRight on='|- _';cases { + "case 1": + z3; + "case 2": +} boogie; boogie; - - - - - +boogie; +boogie; +boogie; +prop;skip; +boogie; boogie; boogie; boogie; boogie; - - - - - +boogie; +prop;skip; +boogie; +boogie; +boogie; boogie; boogie; boogie; boogie; boogie; - +boogie; boogie; - - - - - - - +prop;skip; +boogie; +boogie; +boogie; +boogie; +prop;boogie; +boogie; boogie; boogie; @@ -186,15 +127,15 @@ boogie; boogie; boogie; -expand on='_ |-';prop;skip;substitute on='|- _';close on='|- _'; +boogie; boogie; boogie; boogie; boogie; - +prop;skip;boogie; boogie; - - -substitute on='let node := node₁ :: _ |-';substitute on='let idx := idx₁ :: node₁ == this.nodeseqq[idx]';substitute on='let idx := idx₁ :: idx <= pos && idx >= 0';substitute on='let idx := idx₁ :: _';substitute on=S.0.0.0.0.0.0.0.0.0.1.0.0;substitute on=S.0.0.0.0.0.0.0.0.0.1.1;substitute on='|- _';substitute on='|- _';substitute on='|- _';substitute on='|- _';skip;substitute on=S.0.1.1;skip;substitute on='|- _';substitute on='|- _';substitute on='|- _';substitute on='|- _';prop;skip;expand on='this.Valid()';prop;skip; +boogie; +boogie; +prop;skip;expand on='this.Valid()'; boogie;