From 472e1b73728e6d8647ccc31b7bc057480637ea0c Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Sat, 12 Oct 2024 17:09:09 +0100 Subject: [PATCH 01/11] Optimize some set ordering checks --- vdmj/src/main/java/com/fujitsu/vdmj/values/SetValue.java | 6 +++--- vdmj/src/main/java/com/fujitsu/vdmj/values/ValueSet.java | 5 +++++ 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/values/SetValue.java b/vdmj/src/main/java/com/fujitsu/vdmj/values/SetValue.java index ba9cc7307..7459ecb3f 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/values/SetValue.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/values/SetValue.java @@ -86,7 +86,7 @@ public UpdatableValue getUpdatable(ValueListenerList listeners) for (Value k: values) { Value v = k.getUpdatable(listeners); - nset.add(v); + nset.addNoSort(v); } return UpdatableValue.factory(new SetValue(nset, false), listeners); @@ -100,7 +100,7 @@ public Value getConstant() for (Value k: values) { Value v = k.getConstant(); - nset.add(v); + nset.addNoSort(v); } return new SetValue(nset, false); @@ -191,7 +191,7 @@ protected Value convertValueTo(TCType to, Context ctxt, TCTypeSet done) throws V for (Value v: values) { - ns.add(v.convertValueTo(setto.setof, ctxt)); + ns.addNoSort(v.convertValueTo(setto.setof, ctxt)); } return new SetValue(ns, true); // Re-sort, as ord_T may be different diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/values/ValueSet.java b/vdmj/src/main/java/com/fujitsu/vdmj/values/ValueSet.java index 947b9027d..f4a165c90 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/values/ValueSet.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/values/ValueSet.java @@ -83,6 +83,11 @@ public ValueSet(Value ...values) add(v); } } + + public boolean isSorted() + { + return isSorted; + } @Override public boolean equals(Object other) From 11ddc0472942f981af88f12af27d39bbeaab0d5a Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Sat, 12 Oct 2024 17:09:45 +0100 Subject: [PATCH 02/11] Correct/clarify leastPower method --- .../quickcheck/visitors/RangeCreator.java | 43 ++++++++++++++----- 1 file changed, 32 insertions(+), 11 deletions(-) diff --git a/quickcheck/src/main/java/quickcheck/visitors/RangeCreator.java b/quickcheck/src/main/java/quickcheck/visitors/RangeCreator.java index a58237251..8efde4894 100644 --- a/quickcheck/src/main/java/quickcheck/visitors/RangeCreator.java +++ b/quickcheck/src/main/java/quickcheck/visitors/RangeCreator.java @@ -114,26 +114,47 @@ protected List powerLimit(ValueSet source, int limit, boolean incEmpty /** * Return the lowest integer power of n that is <= limit. If n < 2, - * just return 1. + * just return limit. + * + * Used to calculate how many field values to generate for an n-field object. + * For example, a three field tuple/record with one value each gives 1x1x1=1 records; + * with two values each it gives 2x2x2=8 values, with three 3x3x3=27 values. So to + * generate up to N values from F field combinations, we need to find the largest n, + * such that n^F < N. + * + * If there is only one field, we can generate N values. */ - protected int leastPower(int n, int limit) + protected int leastPower(int F, int N) { - int power = 1; - - if (n > 1) + if (F > 1) { - int value = n; + int n = 2; - while (value < limit) + while (power(n, F) < N) { - value = value * n; - power++; + n++; } + + return n-1; + } + else + { + return N; } - - return power; } + private long power(int n, int p) + { + long result = n; + + for (int i=1; i Date: Sun, 13 Oct 2024 11:45:01 +0100 Subject: [PATCH 03/11] Fix RangeCreator leastPower again --- .../quickcheck/visitors/RangeCreator.java | 22 +++++-------------- 1 file changed, 6 insertions(+), 16 deletions(-) diff --git a/quickcheck/src/main/java/quickcheck/visitors/RangeCreator.java b/quickcheck/src/main/java/quickcheck/visitors/RangeCreator.java index 8efde4894..507d193c7 100644 --- a/quickcheck/src/main/java/quickcheck/visitors/RangeCreator.java +++ b/quickcheck/src/main/java/quickcheck/visitors/RangeCreator.java @@ -128,32 +128,22 @@ protected int leastPower(int F, int N) { if (F > 1) { - int n = 2; + int power = 1; + int value = F; - while (power(n, F) < N) + while (value < N) { - n++; + value = value * F; + power++; } - return n-1; + return power - 1; } else { return N; } } - - private long power(int n, int p) - { - long result = n; - - for (int i=1; i Date: Sun, 13 Oct 2024 11:45:18 +0100 Subject: [PATCH 04/11] Add some sorted ValueList defence --- vdmj/src/main/java/com/fujitsu/vdmj/values/SetValue.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/values/SetValue.java b/vdmj/src/main/java/com/fujitsu/vdmj/values/SetValue.java index 7459ecb3f..76db5be81 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/values/SetValue.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/values/SetValue.java @@ -89,7 +89,7 @@ public UpdatableValue getUpdatable(ValueListenerList listeners) nset.addNoSort(v); } - return UpdatableValue.factory(new SetValue(nset, false), listeners); + return UpdatableValue.factory(new SetValue(nset, !values.isSorted()), listeners); } @Override @@ -103,7 +103,7 @@ public Value getConstant() nset.addNoSort(v); } - return new SetValue(nset, false); + return new SetValue(nset, !values.isSorted()); } @Override @@ -194,7 +194,7 @@ protected Value convertValueTo(TCType to, Context ctxt, TCTypeSet done) throws V ns.addNoSort(v.convertValueTo(setto.setof, ctxt)); } - return new SetValue(ns, true); // Re-sort, as ord_T may be different + return new SetValue(ns, true); // Re-sort, as new type's ord_T may be different } else { From 05330184bc58569e7d1c42381b482e37eac590e4 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Sun, 13 Oct 2024 14:52:47 +0100 Subject: [PATCH 05/11] Clean up PONoCheck context and operation POs --- .../POClassInvariantDefinition.java | 3 - .../POExplicitOperationDefinition.java | 77 ++++++++----------- .../POImplicitOperationDefinition.java | 14 +--- .../vdmj/po/statements/POAlwaysStatement.java | 4 - .../vdmj/po/statements/POTrapStatement.java | 4 - .../visitors/POStatementStateFinder.java | 3 +- .../pog/OperationPostConditionObligation.java | 2 + .../com/fujitsu/vdmj/pog/POContextStack.java | 17 ---- .../fujitsu/vdmj/pog/PONoCheckContext.java | 34 -------- .../com/fujitsu/vdmj/pog/ProofObligation.java | 11 +-- .../fujitsu/vdmj/pog/ProofObligationList.java | 6 +- .../vdmj/pog/StateInvariantObligation.java | 3 + .../fujitsu/vdmj/pog/SubTypeObligation.java | 1 + .../com/fujitsu/vdmj/values/ValueSet.java | 22 +++++- .../java/com/fujitsu/vdmj/junit/PogTest.java | 4 +- 15 files changed, 71 insertions(+), 134 deletions(-) delete mode 100644 vdmj/src/main/java/com/fujitsu/vdmj/pog/PONoCheckContext.java diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassInvariantDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassInvariantDefinition.java index c99e887ff..32bf182df 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassInvariantDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassInvariantDefinition.java @@ -27,7 +27,6 @@ import com.fujitsu.vdmj.po.definitions.visitors.PODefinitionVisitor; import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.pog.POContextStack; -import com.fujitsu.vdmj.pog.PONoCheckContext; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.StateInvariantObligation; import com.fujitsu.vdmj.tc.lex.TCNameToken; @@ -69,9 +68,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment if (!classDefinition.hasConstructors) { - ctxt.push(new PONoCheckContext()); list.add(new StateInvariantObligation(this, ctxt)); - ctxt.pop(); } return list; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitOperationDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitOperationDefinition.java index 5030f0834..88c534cf7 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitOperationDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitOperationDefinition.java @@ -40,7 +40,6 @@ import com.fujitsu.vdmj.pog.POContextStack; import com.fujitsu.vdmj.pog.POFunctionDefinitionContext; import com.fujitsu.vdmj.pog.POImpliesContext; -import com.fujitsu.vdmj.pog.PONoCheckContext; import com.fujitsu.vdmj.pog.POOperationDefinitionContext; import com.fujitsu.vdmj.pog.ParameterPatternObligation; import com.fujitsu.vdmj.pog.ProofObligationList; @@ -159,83 +158,67 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment obligations.addAll(postdef.getProofObligations(ctxt, env)); } - ctxt.push(new PONoCheckContext()); obligations.add(new OperationPostConditionObligation(this, ctxt)); - ctxt.pop(); } boolean updatesState = body.updatesState(); if (stateDefinition != null) { - if (!updatesState) - { - ctxt.push(new POOperationDefinitionContext(this, (precondition != null), stateDefinition, true)); - obligations.addAll(body.getProofObligations(ctxt, null, env)); - ctxt.pop(); - } - else + ctxt.push(new POOperationDefinitionContext(this, (precondition != null), stateDefinition, true)); + ProofObligationList oblist = body.getProofObligations(ctxt, null, env); + ctxt.pop(); + + if (updatesState) { - ctxt.push(new PONoCheckContext()); - ctxt.push(new POOperationDefinitionContext(this, (precondition != null), stateDefinition, true)); - obligations.addAll(body.getProofObligations(ctxt, null, env)); - ctxt.pop(); - ctxt.pop(); + oblist.markUnchecked("Body updates state"); } + + obligations.addAll(oblist); } else if (classDefinition != null) { - if (Settings.release == Release.VDM_10) // Uses the obj_C pattern + ctxt.push(new POOperationDefinitionContext(this, (precondition != null), classDefinition, true)); + ProofObligationList oblist = body.getProofObligations(ctxt, null, env); + ctxt.pop(); + + if (Settings.release == Release.VDM_10) // Uses the obj_C pattern in OperationDefContext + { + oblist.markUnchecked("Obigation requires VDM10"); + } + else if (updatesState) { - if (precondition == null && !updatesState) - { - ctxt.push(new POOperationDefinitionContext(this, false, classDefinition, true)); - obligations.addAll(body.getProofObligations(ctxt, null, env)); - ctxt.pop(); - } - else // Can't check "pre_op(args, new X(args)) => ..." - { - ctxt.push(new PONoCheckContext()); - ctxt.push(new POOperationDefinitionContext(this, true, classDefinition, true)); - obligations.addAll(body.getProofObligations(ctxt, null, env)); - ctxt.pop(); - ctxt.pop(); - } + oblist.markUnchecked("Body updates state"); } + + obligations.addAll(oblist); } else // Flat spec with no state defined { - if (!updatesState) - { - ctxt.push(new POOperationDefinitionContext(this, (precondition != null), null, true)); - obligations.addAll(body.getProofObligations(ctxt, null, env)); - ctxt.pop(); - } - else + ctxt.push(new POOperationDefinitionContext(this, (precondition != null), null, true)); + ProofObligationList oblist = body.getProofObligations(ctxt, null, env); + ctxt.pop(); + + if (updatesState) { - ctxt.push(new PONoCheckContext()); - ctxt.push(new POOperationDefinitionContext(this, (precondition != null), null, true)); - obligations.addAll(body.getProofObligations(ctxt, null, env)); - ctxt.pop(); - ctxt.pop(); + oblist.markUnchecked("Body updates state"); } + + obligations.addAll(oblist); } if (isConstructor && classDefinition != null && classDefinition.invariant != null) { - ctxt.push(new PONoCheckContext()); obligations.add(new StateInvariantObligation(this, ctxt)); - ctxt.pop(); } if (!isConstructor && !TypeComparator.isSubType(actualResult, type.result)) { - ctxt.push(new PONoCheckContext()); - obligations.add(new SubTypeObligation(this, actualResult, ctxt)); - ctxt.pop(); + obligations.add(new SubTypeObligation(this, actualResult, ctxt). + markUnchecked("Unchecked in operations")); } if (annotations != null) annotations.poAfter(this, obligations, ctxt); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitOperationDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitOperationDefinition.java index 5b14eaa99..36b451efc 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitOperationDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitOperationDefinition.java @@ -45,7 +45,6 @@ import com.fujitsu.vdmj.pog.POContextStack; import com.fujitsu.vdmj.pog.POFunctionDefinitionContext; import com.fujitsu.vdmj.pog.POImpliesContext; -import com.fujitsu.vdmj.pog.PONoCheckContext; import com.fujitsu.vdmj.pog.POOperationDefinitionContext; import com.fujitsu.vdmj.pog.ParameterPatternObligation; import com.fujitsu.vdmj.pog.ProofObligationList; @@ -184,18 +183,14 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment obligations.addAll(postdef.getProofObligations(ctxt, env)); } - ctxt.push(new PONoCheckContext()); obligations.add(new OperationPostConditionObligation(this, ctxt)); - ctxt.pop(); } if (body != null) { if (body.updatesState()) { - ctxt.push(new PONoCheckContext()); - obligations.addAll(body.getProofObligations(ctxt, null, env)); - ctxt.pop(); + obligations.addAll(body.getProofObligations(ctxt, null, env).markUnchecked("Body updates state")); } else { @@ -206,17 +201,14 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment classDefinition != null && classDefinition.invariant != null) { - ctxt.push(new PONoCheckContext()); obligations.add(new StateInvariantObligation(this, ctxt)); - ctxt.pop(); } if (!isConstructor && !TypeComparator.isSubType(actualResult, type.result)) { - ctxt.push(new PONoCheckContext()); - obligations.add(new SubTypeObligation(this, actualResult, ctxt)); - ctxt.pop(); + obligations.add(new SubTypeObligation(this, actualResult, ctxt). + markUnchecked("Unchecked in operations")); } } else diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAlwaysStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAlwaysStatement.java index ca154a750..fcfeea6a9 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAlwaysStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAlwaysStatement.java @@ -27,7 +27,6 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor; import com.fujitsu.vdmj.pog.POContextStack; -import com.fujitsu.vdmj.pog.PONoCheckContext; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -54,10 +53,7 @@ public String toString() @Override public ProofObligationList getProofObligations(POContextStack ctxt, POContextStack globals, Environment env) { - ctxt.push(new PONoCheckContext()); ProofObligationList obligations = always.getProofObligations(ctxt, globals, env); - ctxt.pop(); - obligations.addAll(body.getProofObligations(ctxt, globals, env)); return obligations; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POTrapStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POTrapStatement.java index da0340931..2df437908 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POTrapStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POTrapStatement.java @@ -31,7 +31,6 @@ import com.fujitsu.vdmj.po.patterns.POTypeBind; import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor; import com.fujitsu.vdmj.pog.POContextStack; -import com.fujitsu.vdmj.pog.PONoCheckContext; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.SeqMemberObligation; import com.fujitsu.vdmj.pog.SetMemberObligation; @@ -87,10 +86,7 @@ else if (patternBind.bind instanceof POSeqBind) list.add(new SeqMemberObligation(bind.pattern.getMatchingExpression(), bind.sequence, ctxt)); } - ctxt.push(new PONoCheckContext()); list.addAll(with.getProofObligations(ctxt, globals, env)); - ctxt.pop(); - list.addAll(body.getProofObligations(ctxt, globals, env)); return list; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/visitors/POStatementStateFinder.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/visitors/POStatementStateFinder.java index 951302cc3..952e33022 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/visitors/POStatementStateFinder.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/visitors/POStatementStateFinder.java @@ -110,7 +110,7 @@ public TCNameSet caseCallObjectStatement(POCallObjectStatement node, Boolean upd @Override public TCNameSet caseLetDefStatement(POLetDefStatement node, Boolean updates) { - TCNameSet all = newCollection(); + TCNameSet all = super.caseLetDefStatement(node, updates); for (PODefinition def: node.localDefs) { @@ -128,7 +128,6 @@ public TCNameSet caseLetDefStatement(POLetDefStatement node, Boolean updates) } } - all.addAll(super.caseLetDefStatement(node, updates)); return all; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/OperationPostConditionObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/OperationPostConditionObligation.java index d73471fb0..f85e3dc79 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/OperationPostConditionObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/OperationPostConditionObligation.java @@ -38,6 +38,7 @@ public OperationPostConditionObligation( { super(op.location, POType.OP_POST_CONDITION, ctxt); source = ctxt.getSource(getExp(op.precondition, op.postcondition, null)); + markUnchecked("Unchecked in operations"); } public OperationPostConditionObligation( @@ -45,6 +46,7 @@ public OperationPostConditionObligation( { super(op.location, POType.OP_POST_CONDITION, ctxt); source = ctxt.getSource(getExp(op.precondition, op.postcondition, op.errors)); + markUnchecked("Unchecked in operations"); } private String getExp(POExpression preexp, POExpression postexp, List errs) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java index b44470d97..11dca4fab 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java @@ -56,23 +56,6 @@ public String getName() return result.toString(); } - - public boolean isCheckable() - { - ListIterator p = this.listIterator(size()); - - while (p.hasPrevious()) - { - POContext c = p.previous(); - - if (c instanceof PONoCheckContext) - { - return false; - } - } - - return true; - } public String getSource(String poSource) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/PONoCheckContext.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/PONoCheckContext.java deleted file mode 100644 index d1505b84e..000000000 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/PONoCheckContext.java +++ /dev/null @@ -1,34 +0,0 @@ -/******************************************************************************* - * - * Copyright (c) 2016 Fujitsu Services Ltd. - * - * Author: Nick Battle - * - * This file is part of VDMJ. - * - * VDMJ is free software: you can redistribute it and/or modify - * it under the terms of the GNU General Public License as published by - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * VDMJ is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with VDMJ. If not, see . - * SPDX-License-Identifier: GPL-3.0-or-later - * - ******************************************************************************/ - -package com.fujitsu.vdmj.pog; - -public class PONoCheckContext extends POContext -{ - @Override - public String getSource() - { - return ""; - } -} 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 e45bf9db1..7f9baee7e 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java @@ -76,7 +76,7 @@ public ProofObligation(LexLocation location, POType kind, POContextStack ctxt) this.status = POStatus.UNPROVED; this.definition = ctxt.getDefinition(); this.number = 0; - this.isCheckable = ctxt.isCheckable(); // Set false for operation POs + this.isCheckable = true; // Set false for some operation POs this.typeParams = ctxt.getTypeParams(); this.annotations = ctxt.getAnnotations(); this.counterexample = null; @@ -84,11 +84,6 @@ public ProofObligation(LexLocation location, POType kind, POContextStack ctxt) this.message = null; this.provedBy = null; - if (!isCheckable) - { - this.status = POStatus.UNCHECKED; // Implies unproved - } - POGetMatchingExpressionVisitor.init(); // Reset the "any" count, before PO creation } @@ -153,11 +148,13 @@ public void setMessage(String message) /** * This is used to mark obligations as unchecked, with a reason. */ - public void markUnchecked(String message) + public ProofObligation markUnchecked(String message) { this.isCheckable = false; this.setStatus(POStatus.UNCHECKED); this.setMessage(message); + + return this; // Convenient for new XYZObligation().markUnchecked("Some reason") } public boolean isExistential() 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 b88af5f9c..ffae916c7 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java @@ -261,13 +261,15 @@ private void typeCheck(ProofObligation obligation, String mname, Environment env } /** - * This is used by POG to mark obligations as unchecked, with a reason. + * This is used by POG to mark all obligations as unchecked, with a reason. */ - public void markUnchecked(String message) + public ProofObligationList markUnchecked(String message) { for (ProofObligation obligation: this) { obligation.markUnchecked(message); } + + return this; // Convenient for getProofObligations(ctxt, env).markUnchecked("Some reason") } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInvariantObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInvariantObligation.java index e407470d1..a1f31aa01 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInvariantObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInvariantObligation.java @@ -72,6 +72,7 @@ public StateInvariantObligation( sb.append(invDefs(def.classDefinition)); source = ctxt.getSource(sb.toString()); + markUnchecked("Unchecked in VDM++"); } public StateInvariantObligation( @@ -86,6 +87,7 @@ public StateInvariantObligation( sb.append(invDefs(def.classDefinition)); source = ctxt.getSource(sb.toString()); + markUnchecked("Unchecked in VDM++"); } public StateInvariantObligation( @@ -100,6 +102,7 @@ public StateInvariantObligation( sb.append(invDefs(def.classDefinition)); source = ctxt.getSource(sb.toString()); + markUnchecked("Unchecked in VDM++"); } private String invDefs(POClassDefinition def) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/SubTypeObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/SubTypeObligation.java index 1e0f20d9a..8a2e976d6 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/SubTypeObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/SubTypeObligation.java @@ -175,6 +175,7 @@ public SubTypeObligation( new TCNameToken(def.location, def.name.getModule(), "RESULT"), null); source = ctxt.getSource(oneType(false, result, def.type.result, actualResult)); + markUnchecked("Undefined for operations"); } public SubTypeObligation( diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/values/ValueSet.java b/vdmj/src/main/java/com/fujitsu/vdmj/values/ValueSet.java index f4a165c90..48c257d55 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/values/ValueSet.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/values/ValueSet.java @@ -95,7 +95,27 @@ public boolean equals(Object other) if (other instanceof ValueSet) { ValueSet os = (ValueSet)other; - return os.size() == size() && os.containsAll(this); + + if (os.size() != size()) + { + return false; + } + else if (isSorted && os.isSorted) + { + for (int i=0; i iv):A &\n (1 = i => \n ((m(1) < 10) =>\n 1 in set dom m)))\n", /* 82 */ "(forall i:int, obj_A(iv |-> iv):A &\n (1 = i => \n (not (m(1) < 10) =>\n 2 in set dom m)))\n", /* 83 */ "(forall i:int, obj_A(iv |-> iv):A &\n (not 1 = i =>\n (2 = i => \n 3 in set dom m)))\n", - /* 84 */ "(forall obj_A(iv |-> iv):A & pre_op2(new A(iv)) =>\n while (x > 0) do ...)\n", - /* 85 */ "(forall obj_A(iv |-> iv):A & pre_op2(new A(iv)) =>\n let iv = (iv + 1) in (iv < 10))\n" + /* 84 */ "(forall obj_A(iv |-> iv):A &\n while (x > 0) do ...)\n", + /* 85 */ "(forall obj_A(iv |-> iv):A &\n let iv = (iv + 1) in (iv < 10))\n", }; public void testPOG() throws Exception From af1595cbfc07761ba3f1a88c7f4490b72c1fb0e5 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Sun, 13 Oct 2024 14:53:06 +0100 Subject: [PATCH 06/11] Add message to UNCHECKED output --- quickcheck/src/main/java/quickcheck/QuickCheck.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/quickcheck/src/main/java/quickcheck/QuickCheck.java b/quickcheck/src/main/java/quickcheck/QuickCheck.java index 91fa512cf..02131348d 100644 --- a/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -408,7 +408,8 @@ public void checkObligation(ProofObligation po, StrategyResults sresults) if (!po.isCheckable) { - infof(POStatus.UNCHECKED, "PO #%d, UNCHECKED\n", po.number); + infof(POStatus.UNCHECKED, "PO #%d, UNCHECKED %s\n", + po.number, (po.message == null ? "" : po.message)); return; } else if (sresults.provedBy != null) From be2ee381d4fc8a2f6785dfed6badd2611c8b5f8f Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Sun, 13 Oct 2024 15:13:27 +0100 Subject: [PATCH 07/11] Make the state invariant function inv_S: S! +> bool --- .../com/fujitsu/vdmj/tc/definitions/TCStateDefinition.java | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCStateDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCStateDefinition.java index b3f46baa3..394462e23 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCStateDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCStateDefinition.java @@ -36,6 +36,7 @@ import com.fujitsu.vdmj.tc.types.TCField; import com.fujitsu.vdmj.tc.types.TCFieldList; import com.fujitsu.vdmj.tc.types.TCFunctionType; +import com.fujitsu.vdmj.tc.types.TCInvariantType; import com.fujitsu.vdmj.tc.types.TCRecordType; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.tc.types.TCTypeList; @@ -271,7 +272,9 @@ private TCExplicitFunctionDefinition getInvDefinition() parameters.add(params); TCTypeList ptypes = new TCTypeList(); - ptypes.add(new TCUnresolvedType(name)); + TCInvariantType param = recordType.copy(true); + ptypes.add(param); + // ptypes.add(new TCUnresolvedType(name)); TCFunctionType ftype = new TCFunctionType(loc, ptypes, false, new TCBooleanType(loc)); TCExplicitFunctionDefinition def = new TCExplicitFunctionDefinition(null, TCAccessSpecifier.DEFAULT, From b1ff432ad9b808495347d16f2fba240d7b530bbf Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Mon, 14 Oct 2024 18:19:24 +0100 Subject: [PATCH 08/11] Tidy proof obligation messages --- quickcheck/src/main/java/quickcheck/QuickCheck.java | 2 +- .../vdmj/in/expressions/INPowerSetExpression.java | 2 +- .../definitions/POExplicitOperationDefinition.java | 13 +++++++------ .../definitions/POImplicitOperationDefinition.java | 6 ++++-- .../vdmj/po/expressions/POCasesExpression.java | 3 ++- .../vdmj/po/statements/POBlockStatement.java | 5 ----- .../vdmj/po/statements/POForAllStatement.java | 3 ++- .../vdmj/po/statements/POForIndexStatement.java | 3 ++- .../vdmj/po/statements/POWhileStatement.java | 3 ++- .../vdmj/pog/OperationPostConditionObligation.java | 4 ++-- .../java/com/fujitsu/vdmj/pog/ProofObligation.java | 13 +++++++++++-- .../com/fujitsu/vdmj/pog/ProofObligationList.java | 5 +++-- .../fujitsu/vdmj/pog/StateInvariantObligation.java | 6 +++--- .../com/fujitsu/vdmj/pog/SubTypeObligation.java | 2 +- .../main/java/com/fujitsu/vdmj/values/ValueSet.java | 12 ------------ 15 files changed, 41 insertions(+), 41 deletions(-) diff --git a/quickcheck/src/main/java/quickcheck/QuickCheck.java b/quickcheck/src/main/java/quickcheck/QuickCheck.java index 02131348d..996748104 100644 --- a/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -409,7 +409,7 @@ public void checkObligation(ProofObligation po, StrategyResults sresults) if (!po.isCheckable) { infof(POStatus.UNCHECKED, "PO #%d, UNCHECKED %s\n", - po.number, (po.message == null ? "" : po.message)); + po.number, (po.message == null ? "" : "(" + po.message + ")")); return; } else if (sresults.provedBy != null) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INPowerSetExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INPowerSetExpression.java index 00e7bfc0b..5e603aae3 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INPowerSetExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INPowerSetExpression.java @@ -65,7 +65,7 @@ public Value eval(Context ctxt) for (ValueSet v: psets) { - rs.addNoCheck(new SetValue(v)); + rs.addNoCheck(new SetValue(v, false)); // Already sorted } // The additions above can take a while, because all of the SetValues are diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitOperationDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitOperationDefinition.java index 88c534cf7..d585df8e1 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitOperationDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitOperationDefinition.java @@ -42,6 +42,7 @@ import com.fujitsu.vdmj.pog.POImpliesContext; import com.fujitsu.vdmj.pog.POOperationDefinitionContext; import com.fujitsu.vdmj.pog.ParameterPatternObligation; +import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.StateInvariantObligation; import com.fujitsu.vdmj.pog.SubTypeObligation; @@ -171,7 +172,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment if (updatesState) { - oblist.markUnchecked("Body updates state"); + oblist.markUnchecked(ProofObligation.BODY_UPDATES_STATE); } obligations.addAll(oblist); @@ -182,13 +183,13 @@ else if (classDefinition != null) ProofObligationList oblist = body.getProofObligations(ctxt, null, env); ctxt.pop(); - if (Settings.release == Release.VDM_10) // Uses the obj_C pattern in OperationDefContext + if (Settings.release != Release.VDM_10) // Uses the obj_C pattern in OperationDefContext { - oblist.markUnchecked("Obigation requires VDM10"); + oblist.markUnchecked(ProofObligation.REQUIRES_VDM10); } else if (updatesState) { - oblist.markUnchecked("Body updates state"); + oblist.markUnchecked(ProofObligation.BODY_UPDATES_STATE); } obligations.addAll(oblist); @@ -201,7 +202,7 @@ else if (updatesState) if (updatesState) { - oblist.markUnchecked("Body updates state"); + oblist.markUnchecked(ProofObligation.BODY_UPDATES_STATE); } obligations.addAll(oblist); @@ -218,7 +219,7 @@ else if (updatesState) !TypeComparator.isSubType(actualResult, type.result)) { obligations.add(new SubTypeObligation(this, actualResult, ctxt). - markUnchecked("Unchecked in operations")); + markUnchecked(ProofObligation.NOT_YET_SUPPORTED)); } if (annotations != null) annotations.poAfter(this, obligations, ctxt); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitOperationDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitOperationDefinition.java index 36b451efc..bb6369e07 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitOperationDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitOperationDefinition.java @@ -47,6 +47,7 @@ import com.fujitsu.vdmj.pog.POImpliesContext; import com.fujitsu.vdmj.pog.POOperationDefinitionContext; import com.fujitsu.vdmj.pog.ParameterPatternObligation; +import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.SatisfiabilityObligation; import com.fujitsu.vdmj.pog.StateInvariantObligation; @@ -190,7 +191,8 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment { if (body.updatesState()) { - obligations.addAll(body.getProofObligations(ctxt, null, env).markUnchecked("Body updates state")); + obligations.addAll(body.getProofObligations(ctxt, null, env). + markUnchecked(ProofObligation.BODY_UPDATES_STATE)); } else { @@ -208,7 +210,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment !TypeComparator.isSubType(actualResult, type.result)) { obligations.add(new SubTypeObligation(this, actualResult, ctxt). - markUnchecked("Unchecked in operations")); + markUnchecked(ProofObligation.NOT_YET_SUPPORTED)); } } else diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POCasesExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POCasesExpression.java index 56107ad78..8c4e8c737 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POCasesExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POCasesExpression.java @@ -29,6 +29,7 @@ import com.fujitsu.vdmj.po.patterns.POIgnorePattern; import com.fujitsu.vdmj.pog.CasesExhaustiveObligation; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.lex.TCNameList; import com.fujitsu.vdmj.tc.types.TCType; @@ -100,7 +101,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment if (!hidden.isEmpty()) { - _obligations.markUnchecked("Obligation patterns contain hidden variables: " + hidden); + _obligations.markUnchecked(ProofObligation.HIDDEN_VARIABLES + ": " + hidden); } obligations.addAll(_obligations); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POBlockStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POBlockStatement.java index 3fc5d8439..b1250728a 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POBlockStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POBlockStatement.java @@ -52,11 +52,6 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POContextSta ctxt.push(new POScopeContext()); obligations.addAll(super.getProofObligations(ctxt, globals, env)); ctxt.pop(); - - if (!assignmentDefs.isEmpty()) - { - obligations.markUnchecked("dcl statement block"); - } return obligations; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForAllStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForAllStatement.java index d7546a039..71cfa5b48 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForAllStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForAllStatement.java @@ -29,6 +29,7 @@ import com.fujitsu.vdmj.po.patterns.POPattern; import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -59,7 +60,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POContextSta { ProofObligationList obligations = set.getProofObligations(ctxt, env); obligations.addAll(statement.getProofObligations(ctxt, globals, env)); - obligations.markUnchecked("Loop statement"); + obligations.markUnchecked(ProofObligation.LOOP_STATEMENT); return obligations; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForIndexStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForIndexStatement.java index 095b3e133..2a2c51c3e 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForIndexStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForIndexStatement.java @@ -29,6 +29,7 @@ import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor; import com.fujitsu.vdmj.pog.POContextStack; import com.fujitsu.vdmj.pog.POScopeContext; +import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.lex.TCNameToken; import com.fujitsu.vdmj.typechecker.Environment; @@ -75,7 +76,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POContextSta obligations.addAll(statement.getProofObligations(ctxt, globals, env)); ctxt.pop(); - obligations.markUnchecked("Loop statement"); + obligations.markUnchecked(ProofObligation.LOOP_STATEMENT); return obligations; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POWhileStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POWhileStatement.java index f010b44d5..ea9814e75 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POWhileStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POWhileStatement.java @@ -28,6 +28,7 @@ import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.WhileLoopObligation; import com.fujitsu.vdmj.typechecker.Environment; @@ -58,7 +59,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POContextSta obligations.add(new WhileLoopObligation(this, ctxt)); obligations.addAll(exp.getProofObligations(ctxt, env)); obligations.addAll(statement.getProofObligations(ctxt, globals, env)); - obligations.markUnchecked("Loop statement"); + obligations.markUnchecked(ProofObligation.LOOP_STATEMENT); return obligations; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/OperationPostConditionObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/OperationPostConditionObligation.java index f85e3dc79..89a98ff55 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/OperationPostConditionObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/OperationPostConditionObligation.java @@ -38,7 +38,7 @@ public OperationPostConditionObligation( { super(op.location, POType.OP_POST_CONDITION, ctxt); source = ctxt.getSource(getExp(op.precondition, op.postcondition, null)); - markUnchecked("Unchecked in operations"); + markUnchecked(ProofObligation.NOT_YET_SUPPORTED); } public OperationPostConditionObligation( @@ -46,7 +46,7 @@ public OperationPostConditionObligation( { super(op.location, POType.OP_POST_CONDITION, ctxt); source = ctxt.getSource(getExp(op.precondition, op.postcondition, op.errors)); - markUnchecked("Unchecked in operations"); + markUnchecked(ProofObligation.NOT_YET_SUPPORTED); } private String getExp(POExpression preexp, POExpression postexp, List errs) 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 7f9baee7e..11cb895f0 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java @@ -46,6 +46,15 @@ abstract public class ProofObligation implements Comparable { + // Arguments for the markUnchecked method. + public static final String NOT_YET_SUPPORTED = "Not yet supported for operations"; + public static final String MISSING_MEASURE = "Obligation for missing measure function"; + public static final String UNCHECKED_VDMPP = "Unchecked in VDM++"; + public static final String HIDDEN_VARIABLES = "Obligation patterns contain hidden variables"; + public static final String REQUIRES_VDM10 = "Obigation requires VDM10"; + public static final String BODY_UPDATES_STATE = "Operation body updates state"; + public static final String LOOP_STATEMENT = "Loop statement encountered"; + public final LexLocation location; public final POType kind; public final String name; @@ -146,7 +155,7 @@ public void setMessage(String message) } /** - * This is used to mark obligations as unchecked, with a reason. + * This is used to mark obligations as unchecked, with a reason code. */ public ProofObligation markUnchecked(String message) { @@ -154,7 +163,7 @@ public ProofObligation markUnchecked(String message) this.setStatus(POStatus.UNCHECKED); this.setMessage(message); - return this; // Convenient for new XYZObligation().markUnchecked("Some reason") + return this; // Convenient for new XYZObligation().markUnchecked(REASON) } public boolean isExistential() 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 ffae916c7..d500e965a 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java @@ -229,7 +229,7 @@ private void typeCheck(ProofObligation obligation, String mname, Environment env { // Probably an implicit missing measure iter.remove(); - obligation.markUnchecked("Obligation for missing measure function"); + obligation.markUnchecked(ProofObligation.MISSING_MEASURE); } break; @@ -261,7 +261,8 @@ private void typeCheck(ProofObligation obligation, String mname, Environment env } /** - * This is used by POG to mark all obligations as unchecked, with a reason. + * This is used by POG to mark all obligations as unchecked, with a reason. Preferably, + * use the reason code string constants in ProofObligation. */ public ProofObligationList markUnchecked(String message) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInvariantObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInvariantObligation.java index a1f31aa01..3ad626911 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInvariantObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInvariantObligation.java @@ -72,7 +72,7 @@ public StateInvariantObligation( sb.append(invDefs(def.classDefinition)); source = ctxt.getSource(sb.toString()); - markUnchecked("Unchecked in VDM++"); + markUnchecked(ProofObligation.UNCHECKED_VDMPP); } public StateInvariantObligation( @@ -87,7 +87,7 @@ public StateInvariantObligation( sb.append(invDefs(def.classDefinition)); source = ctxt.getSource(sb.toString()); - markUnchecked("Unchecked in VDM++"); + markUnchecked(ProofObligation.UNCHECKED_VDMPP); } public StateInvariantObligation( @@ -102,7 +102,7 @@ public StateInvariantObligation( sb.append(invDefs(def.classDefinition)); source = ctxt.getSource(sb.toString()); - markUnchecked("Unchecked in VDM++"); + markUnchecked(ProofObligation.UNCHECKED_VDMPP); } private String invDefs(POClassDefinition def) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/SubTypeObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/SubTypeObligation.java index 8a2e976d6..fcc1318a2 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/SubTypeObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/SubTypeObligation.java @@ -175,7 +175,7 @@ public SubTypeObligation( new TCNameToken(def.location, def.name.getModule(), "RESULT"), null); source = ctxt.getSource(oneType(false, result, def.type.result, actualResult)); - markUnchecked("Undefined for operations"); + markUnchecked(ProofObligation.NOT_YET_SUPPORTED); } public SubTypeObligation( diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/values/ValueSet.java b/vdmj/src/main/java/com/fujitsu/vdmj/values/ValueSet.java index 48c257d55..d7eece16d 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/values/ValueSet.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/values/ValueSet.java @@ -100,18 +100,6 @@ public boolean equals(Object other) { return false; } - else if (isSorted && os.isSorted) - { - for (int i=0; i Date: Tue, 15 Oct 2024 10:56:17 +0100 Subject: [PATCH 09/11] Improve ValueSet sorted checks --- .../visitors/FixedRangeCreator.java | 8 ++--- .../in/expressions/INIndicesExpression.java | 4 +-- .../in/expressions/INPowerSetExpression.java | 2 +- .../in/expressions/INSetRangeExpression.java | 2 +- .../com/fujitsu/vdmj/values/SetValue.java | 6 ++-- .../com/fujitsu/vdmj/values/ValueSet.java | 33 +++++++++++++++---- 6 files changed, 37 insertions(+), 18 deletions(-) diff --git a/quickcheck/src/main/java/quickcheck/visitors/FixedRangeCreator.java b/quickcheck/src/main/java/quickcheck/visitors/FixedRangeCreator.java index 48df99a0e..b008147b8 100644 --- a/quickcheck/src/main/java/quickcheck/visitors/FixedRangeCreator.java +++ b/quickcheck/src/main/java/quickcheck/visitors/FixedRangeCreator.java @@ -193,7 +193,7 @@ public ValueSet caseNaturalOneType(TCNaturalOneType node, Integer limit) { try { - result.addNoSort(new NaturalOneValue(a)); + result.addSorted(new NaturalOneValue(a)); } catch (Exception e) { @@ -213,7 +213,7 @@ public ValueSet caseNaturalType(TCNaturalType node, Integer limit) { try { - result.addNoSort(new NaturalValue(a)); + result.addSorted(new NaturalValue(a)); } catch (Exception e) { @@ -235,11 +235,11 @@ public ValueSet caseIntegerType(TCIntegerType node, Integer limit) case 1: return new ValueSet(new IntegerValue(0)); default: int a = -limit/2; - result.addNoSort(new IntegerValue(a++)); + result.addSorted(new IntegerValue(a++)); while (result.size() < limit) { - result.addNoSort(new IntegerValue(a)); + result.addSorted(new IntegerValue(a)); a++; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INIndicesExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INIndicesExpression.java index 507c74a1b..6264e0478 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INIndicesExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INIndicesExpression.java @@ -61,10 +61,10 @@ public Value eval(Context ctxt) for (int i=1; i<= seq.size(); i++) { - result.addNoCheck(new NaturalOneValue(i)); + result.addSorted(new NaturalOneValue(i)); } - return new SetValue(result); + return new SetValue(result, false); } catch (ValueException e) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INPowerSetExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INPowerSetExpression.java index 5e603aae3..3d7d4532a 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INPowerSetExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INPowerSetExpression.java @@ -65,7 +65,7 @@ public Value eval(Context ctxt) for (ValueSet v: psets) { - rs.addNoCheck(new SetValue(v, false)); // Already sorted + rs.addSorted(new SetValue(v, false)); // Already sorted } // The additions above can take a while, because all of the SetValues are diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INSetRangeExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INSetRangeExpression.java index 1e2d40ccd..cd754f21a 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INSetRangeExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INSetRangeExpression.java @@ -65,7 +65,7 @@ public Value eval(Context ctxt) for (long i=from; i<= to; i++) { - set.addNoCheck(new IntegerValue(i)); + set.addSorted(new IntegerValue(i)); } return new SetValue(set, false); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/values/SetValue.java b/vdmj/src/main/java/com/fujitsu/vdmj/values/SetValue.java index 76db5be81..2aca04ca1 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/values/SetValue.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/values/SetValue.java @@ -86,7 +86,7 @@ public UpdatableValue getUpdatable(ValueListenerList listeners) for (Value k: values) { Value v = k.getUpdatable(listeners); - nset.addNoSort(v); + nset.addSorted(v, values.isSorted()); } return UpdatableValue.factory(new SetValue(nset, !values.isSorted()), listeners); @@ -100,7 +100,7 @@ public Value getConstant() for (Value k: values) { Value v = k.getConstant(); - nset.addNoSort(v); + nset.addSorted(v, values.isSorted()); } return new SetValue(nset, !values.isSorted()); @@ -191,7 +191,7 @@ protected Value convertValueTo(TCType to, Context ctxt, TCTypeSet done) throws V for (Value v: values) { - ns.addNoSort(v.convertValueTo(setto.setof, ctxt)); + ns.addUnsorted(v.convertValueTo(setto.setof, ctxt)); } return new SetValue(ns, true); // Re-sort, as new type's ord_T may be different diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/values/ValueSet.java b/vdmj/src/main/java/com/fujitsu/vdmj/values/ValueSet.java index d7eece16d..805db6fe0 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/values/ValueSet.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/values/ValueSet.java @@ -100,6 +100,18 @@ public boolean equals(Object other) { return false; } + else if (isSorted && os.isSorted) + { + for (int i=0; i permutedSets() for (int i=0; i powerSet(Breakpoint breakpoint, Context ctxt) for (int i=0; i= 100) From f28f66426e423af6ce373687db554173697bb951 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Tue, 15 Oct 2024 14:45:41 +0100 Subject: [PATCH 10/11] Tidy block statements with dcl definitions --- .../vdmj/po/definitions/POAssignmentDefinition.java | 3 +-- .../definitions/visitors/PODefinitionStateFinder.java | 11 +++++++++++ .../fujitsu/vdmj/po/statements/POBlockStatement.java | 6 ++++++ .../java/com/fujitsu/vdmj/pog/POLetDefContext.java | 10 ++++++++++ .../java/com/fujitsu/vdmj/pog/ProofObligation.java | 1 + 5 files changed, 29 insertions(+), 2 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POAssignmentDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POAssignmentDefinition.java index c1a878ecd..d06f98790 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POAssignmentDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POAssignmentDefinition.java @@ -73,8 +73,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment if (!TypeComparator.isSubType(ctxt.checkType(expression, expType), type)) { - obligations.add( - new SubTypeObligation(expression, type, expType, ctxt)); + obligations.add(new SubTypeObligation(expression, type, expType, ctxt)); } return obligations; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/visitors/PODefinitionStateFinder.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/visitors/PODefinitionStateFinder.java index 302f4394e..022294de4 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/visitors/PODefinitionStateFinder.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/visitors/PODefinitionStateFinder.java @@ -25,6 +25,7 @@ package com.fujitsu.vdmj.po.definitions.visitors; import com.fujitsu.vdmj.po.POVisitorSet; +import com.fujitsu.vdmj.po.definitions.POAssignmentDefinition; import com.fujitsu.vdmj.po.definitions.PODefinition; import com.fujitsu.vdmj.tc.lex.TCNameSet; import com.fujitsu.vdmj.tc.lex.TCNameToken; @@ -39,6 +40,16 @@ public PODefinitionStateFinder(POVisitorSet vis this.visitorSet = visitors; } + @Override + public TCNameSet caseAssignmentDefinition(POAssignmentDefinition node, Boolean updates) + { + TCNameSet all = newCollection(); + + all.add(node.name); // eg. dcl declarations. + + return all; + } + @Override protected TCNameSet newCollection() { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POBlockStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POBlockStatement.java index b1250728a..afa37109f 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POBlockStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POBlockStatement.java @@ -29,6 +29,7 @@ import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor; import com.fujitsu.vdmj.pog.POContextStack; import com.fujitsu.vdmj.pog.POScopeContext; +import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -52,6 +53,11 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POContextSta ctxt.push(new POScopeContext()); obligations.addAll(super.getProofObligations(ctxt, globals, env)); ctxt.pop(); + + if (!assignmentDefs.isEmpty()) + { + obligations.markUnchecked(ProofObligation.DCL_STATEMENT); + } return obligations; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLetDefContext.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLetDefContext.java index 90626b8bc..39d7c0d0c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLetDefContext.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POLetDefContext.java @@ -24,8 +24,11 @@ package com.fujitsu.vdmj.pog; +import com.fujitsu.vdmj.po.definitions.POAssignmentDefinition; import com.fujitsu.vdmj.po.definitions.PODefinition; import com.fujitsu.vdmj.po.definitions.PODefinitionList; +import com.fujitsu.vdmj.po.definitions.POValueDefinition; +import com.fujitsu.vdmj.po.patterns.POIdentifierPattern; public class POLetDefContext extends POContext { @@ -42,6 +45,13 @@ public POLetDefContext(PODefinition localDef) this.localDefs.add(localDef); } + public POLetDefContext(POAssignmentDefinition dcl) + { + this.localDefs = new PODefinitionList(); + this.localDefs.add(new POValueDefinition(null, + new POIdentifierPattern(dcl.name), dcl.type, dcl.expression, dcl.expType, new PODefinitionList())); + } + @Override public boolean isScopeBoundary() { 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 11cb895f0..4e1dc129f 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java @@ -54,6 +54,7 @@ abstract public class ProofObligation implements Comparable public static final String REQUIRES_VDM10 = "Obigation requires VDM10"; public static final String BODY_UPDATES_STATE = "Operation body updates state"; public static final String LOOP_STATEMENT = "Loop statement encountered"; + public static final String DCL_STATEMENT = "Block contains dcl assignments"; public final LexLocation location; public final POType kind; From e582e83f4d101f5ad9d8fc79e5df083bd8bcf5a1 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Tue, 15 Oct 2024 17:23:34 +0100 Subject: [PATCH 11/11] Attempt to handle state updates in statement blocks --- .../POExplicitOperationDefinition.java | 7 ++- .../POImplicitOperationDefinition.java | 59 ++++++++++++++++--- .../po/statements/POSimpleBlockStatement.java | 16 ++++- .../com/fujitsu/vdmj/pog/ProofObligation.java | 1 + 4 files changed, 72 insertions(+), 11 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitOperationDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitOperationDefinition.java index d585df8e1..707f01fec 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitOperationDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitOperationDefinition.java @@ -35,6 +35,7 @@ import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.po.patterns.POPattern; import com.fujitsu.vdmj.po.patterns.POPatternList; +import com.fujitsu.vdmj.po.statements.POSimpleBlockStatement; import com.fujitsu.vdmj.po.statements.POStatement; import com.fujitsu.vdmj.pog.OperationPostConditionObligation; import com.fujitsu.vdmj.pog.POContextStack; @@ -162,7 +163,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment obligations.add(new OperationPostConditionObligation(this, ctxt)); } - boolean updatesState = body.updatesState(); + boolean updatesState = !(body instanceof POSimpleBlockStatement) && body.updatesState(); if (stateDefinition != null) { @@ -187,6 +188,10 @@ else if (classDefinition != null) { oblist.markUnchecked(ProofObligation.REQUIRES_VDM10); } + else if (precondition != null) // pre_op undefined in VDM++ + { + oblist.markUnchecked(ProofObligation.UNCHECKED_VDMPP); + } else if (updatesState) { oblist.markUnchecked(ProofObligation.BODY_UPDATES_STATE); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitOperationDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitOperationDefinition.java index bb6369e07..e191a7f86 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitOperationDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitOperationDefinition.java @@ -37,6 +37,7 @@ import com.fujitsu.vdmj.po.patterns.POPatternList; import com.fujitsu.vdmj.po.statements.POErrorCaseList; import com.fujitsu.vdmj.po.statements.POExternalClauseList; +import com.fujitsu.vdmj.po.statements.POSimpleBlockStatement; import com.fujitsu.vdmj.po.statements.POStatement; import com.fujitsu.vdmj.po.types.POPatternListTypePair; import com.fujitsu.vdmj.po.types.POPatternListTypePairList; @@ -79,7 +80,7 @@ public class POImplicitOperationDefinition extends PODefinition public final POExplicitFunctionDefinition predef; public final POExplicitFunctionDefinition postdef; public final TCType actualResult; - public final PODefinition state; + public final PODefinition stateDefinition; public final boolean isConstructor; public POImplicitOperationDefinition(POAnnotationList annotations, @@ -111,7 +112,7 @@ public POImplicitOperationDefinition(POAnnotationList annotations, this.predef = predef; this.postdef = postdef; this.actualResult = actualResult; - this.state = stateDefinition; + this.stateDefinition = stateDefinition; this.isConstructor = isConstructor; } @@ -189,14 +190,54 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment if (body != null) { - if (body.updatesState()) + boolean updatesState = !(body instanceof POSimpleBlockStatement) && body.updatesState(); + + if (stateDefinition != null) { - obligations.addAll(body.getProofObligations(ctxt, null, env). - markUnchecked(ProofObligation.BODY_UPDATES_STATE)); + ctxt.push(new POOperationDefinitionContext(this, (precondition != null), stateDefinition, true)); + ProofObligationList oblist = body.getProofObligations(ctxt, null, env); + ctxt.pop(); + + if (updatesState) + { + oblist.markUnchecked(ProofObligation.BODY_UPDATES_STATE); + } + + obligations.addAll(oblist); } - else + else if (classDefinition != null) { - obligations.addAll(body.getProofObligations(ctxt, null, env)); + ctxt.push(new POOperationDefinitionContext(this, (precondition != null), classDefinition, true)); + ProofObligationList oblist = body.getProofObligations(ctxt, null, env); + ctxt.pop(); + + if (Settings.release != Release.VDM_10) // Uses the obj_C pattern in OperationDefContext + { + oblist.markUnchecked(ProofObligation.REQUIRES_VDM10); + } + else if (precondition != null) // pre_op undefined in VDM++ + { + oblist.markUnchecked(ProofObligation.UNCHECKED_VDMPP); + } + else if (updatesState) + { + oblist.markUnchecked(ProofObligation.BODY_UPDATES_STATE); + } + + obligations.addAll(oblist); + } + else // Flat spec with no state defined + { + ctxt.push(new POOperationDefinitionContext(this, (precondition != null), null, true)); + ProofObligationList oblist = body.getProofObligations(ctxt, null, env); + ctxt.pop(); + + if (updatesState) + { + oblist.markUnchecked(ProofObligation.BODY_UPDATES_STATE); + } + + obligations.addAll(oblist); } if (isConstructor && @@ -218,8 +259,8 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment if (postcondition != null && Settings.dialect == Dialect.VDM_SL && Settings.release == Release.VDM_10) // Uses obj_C pattern { - ctxt.push(new POOperationDefinitionContext(this, false, state, false)); - obligations.add(new SatisfiabilityObligation(this, state, ctxt)); + ctxt.push(new POOperationDefinitionContext(this, false, stateDefinition, false)); + obligations.add(new SatisfiabilityObligation(this, stateDefinition, ctxt)); ctxt.pop(); } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POSimpleBlockStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POSimpleBlockStatement.java index 21770d820..984c89a04 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POSimpleBlockStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POSimpleBlockStatement.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -68,10 +69,23 @@ public String toString() public ProofObligationList getProofObligations(POContextStack ctxt, POContextStack globals, Environment env) { ProofObligationList obligations = new ProofObligationList(); + boolean hasUpdatedState = false; for (POStatement stmt: statements) { - obligations.addAll(stmt.getProofObligations(ctxt, globals, env)); + ProofObligationList oblist = stmt.getProofObligations(ctxt, globals, env); + + if (stmt.updatesState()) + { + hasUpdatedState = true; + oblist.markUnchecked(ProofObligation.BODY_UPDATES_STATE); + } + else if (stmt.readsState() && hasUpdatedState) + { + oblist.markUnchecked(ProofObligation.HAS_UPDATED_STATE); + } + + obligations.addAll(oblist); } return obligations; 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 4e1dc129f..7414b9731 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java @@ -55,6 +55,7 @@ abstract public class ProofObligation implements Comparable public static final String BODY_UPDATES_STATE = "Operation body updates state"; public static final String LOOP_STATEMENT = "Loop statement encountered"; public static final String DCL_STATEMENT = "Block contains dcl assignments"; + public static final String HAS_UPDATED_STATE = "Previous statements updated state"; public final LexLocation location; public final POType kind;