From 1f61aa879c804281f6f879876d02b94fc2fbd5bd Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Sat, 19 Oct 2024 11:20:20 +0100 Subject: [PATCH 1/9] Refresh SL imports after VALUES pass of type checker --- .../vdmj/typechecker/ModuleTypeChecker.java | 21 +++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/typechecker/ModuleTypeChecker.java b/vdmj/src/main/java/com/fujitsu/vdmj/typechecker/ModuleTypeChecker.java index b83d49fb9..6b3489f4b 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/typechecker/ModuleTypeChecker.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/typechecker/ModuleTypeChecker.java @@ -233,6 +233,23 @@ public void typeCheck() m.annotations.tcAfter(m, e); } } + + // After the VALUES pass, ValueDefinitions will have replaced their TCUntypedDefinition "defs" + // with typed TCLocalDefinitions, so we refresh the export/importDefs to allow later passes + // to see the correct types of imported definitions. + + if (pass == Pass.VALUES) + { + for (TCModule m: modules) + { + m.processExports(); // Re-populate exports + } + + for (TCModule m: modules) + { + m.processImports(modules); // Re-populate importDefs + } + } } // Prepare to look for recursive loops @@ -243,12 +260,12 @@ public void typeCheck() for (TCModule m: modules) { - m.processExports(); // Re-populate exports + m.processExports(); // Re-populate exports again } for (TCModule m: modules) { - m.processImports(modules); // Re-populate importDefs + m.processImports(modules); // Re-populate importDefs again try { From 36e533fe2965253c482b1e4597e235f2ec355f11 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Sat, 19 Oct 2024 17:35:27 +0100 Subject: [PATCH 2/9] Added binds to state finders and process designators properly --- .../patterns/visitors/POBindStateFinder.java | 52 +++++++++++ .../visitors/POMultipleBindStateFinder.java | 52 +++++++++++ .../visitors/POStatementStateFinder.java | 89 ++++++++++++++----- 3 files changed, 173 insertions(+), 20 deletions(-) create mode 100644 vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/POBindStateFinder.java create mode 100644 vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/POMultipleBindStateFinder.java diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/POBindStateFinder.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/POBindStateFinder.java new file mode 100644 index 000000000..b777b6fb2 --- /dev/null +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/POBindStateFinder.java @@ -0,0 +1,52 @@ +/******************************************************************************* + * + * Copyright (c) 2024 Nick Battle. + * + * 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.po.patterns.visitors; + +import com.fujitsu.vdmj.po.POVisitorSet; +import com.fujitsu.vdmj.po.patterns.POBind; +import com.fujitsu.vdmj.tc.lex.TCNameSet; +import com.fujitsu.vdmj.tc.lex.TCNameToken; + +/** + * A visitor set to explore the PO tree and return the state names accessed. + */ +public class POBindStateFinder extends POLeafBindVisitor +{ + public POBindStateFinder(POVisitorSet visitors) + { + this.visitorSet = visitors; + } + + @Override + protected TCNameSet newCollection() + { + return new TCNameSet(); + } + + @Override + public TCNameSet caseBind(POBind node, Boolean arg) + { + return newCollection(); + } +} diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/POMultipleBindStateFinder.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/POMultipleBindStateFinder.java new file mode 100644 index 000000000..cd3041dca --- /dev/null +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/POMultipleBindStateFinder.java @@ -0,0 +1,52 @@ +/******************************************************************************* + * + * Copyright (c) 2024 Nick Battle. + * + * 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.po.patterns.visitors; + +import com.fujitsu.vdmj.po.POVisitorSet; +import com.fujitsu.vdmj.po.patterns.POMultipleBind; +import com.fujitsu.vdmj.tc.lex.TCNameSet; +import com.fujitsu.vdmj.tc.lex.TCNameToken; + +/** + * A visitor set to explore the PO tree and return the state names accessed. + */ +public class POMultipleBindStateFinder extends POLeafMultipleBindVisitor +{ + public POMultipleBindStateFinder(POVisitorSet visitors) + { + this.visitorSet = visitors; + } + + @Override + protected TCNameSet newCollection() + { + return new TCNameSet(); + } + + @Override + public TCNameSet caseMultipleBind(POMultipleBind node, Boolean arg) + { + return newCollection(); + } +} 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 952e33022..7adef8a01 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 @@ -24,16 +24,22 @@ package com.fujitsu.vdmj.po.statements.visitors; +import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.POVisitorSet; import com.fujitsu.vdmj.po.definitions.PODefinition; import com.fujitsu.vdmj.po.definitions.POValueDefinition; import com.fujitsu.vdmj.po.definitions.visitors.PODefinitionStateFinder; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionStateFinder; +import com.fujitsu.vdmj.po.patterns.visitors.POBindStateFinder; +import com.fujitsu.vdmj.po.patterns.visitors.POMultipleBindStateFinder; import com.fujitsu.vdmj.po.statements.POAssignmentStatement; import com.fujitsu.vdmj.po.statements.POCallObjectStatement; import com.fujitsu.vdmj.po.statements.POCallStatement; +import com.fujitsu.vdmj.po.statements.POFieldDesignator; import com.fujitsu.vdmj.po.statements.POIdentifierDesignator; import com.fujitsu.vdmj.po.statements.POLetDefStatement; +import com.fujitsu.vdmj.po.statements.POMapSeqDesignator; +import com.fujitsu.vdmj.po.statements.POStateDesignator; import com.fujitsu.vdmj.po.statements.POStatement; import com.fujitsu.vdmj.tc.lex.TCNameSet; import com.fujitsu.vdmj.tc.lex.TCNameToken; @@ -44,6 +50,8 @@ */ public class POStatementStateFinder extends POLeafStatementVisitor { + private static TCNameToken EVERYTHING = new TCNameToken(LexLocation.ANY, "*", "*"); + public POStatementStateFinder() { super(false); @@ -53,12 +61,11 @@ public POStatementStateFinder() @Override protected void setVisitors() { + statementVisitor = POStatementStateFinder.this; definitionVisitor = new PODefinitionStateFinder(this); expressionVisitor = new POExpressionStateFinder(this); - statementVisitor = POStatementStateFinder.this; - patternVisitor = null; - bindVisitor = null; - multiBindVisitor = null; + bindVisitor = new POBindStateFinder(this); + multiBindVisitor = new POMultipleBindStateFinder(this); } @Override @@ -72,30 +79,21 @@ protected TCNameSet newCollection() @Override public TCNameSet caseAssignmentStatement(POAssignmentStatement node, Boolean updates) { - TCNameSet all = newCollection(); - if (updates) { - if (node.target instanceof POIdentifierDesignator) - { - POIdentifierDesignator id = (POIdentifierDesignator)node.target; - all.add(id.name); - } - else - { - // Updates something... - all.add(new TCNameToken(node.location, "?", node.target.toString())); - } + return designatorUpdates(node.target); + } + else + { + return designatorReads(node.target); } - - return all; } @Override public TCNameSet caseCallStatement(POCallStatement node, Boolean updates) { TCNameSet all = newCollection(); - all.add(new TCNameToken(node.location, "?", "?")); // Not state, but assumed to access state. + all.add(EVERYTHING); // Not state, but assumed to access state. return all; } @@ -103,7 +101,7 @@ public TCNameSet caseCallStatement(POCallStatement node, Boolean updates) public TCNameSet caseCallObjectStatement(POCallObjectStatement node, Boolean updates) { TCNameSet all = newCollection(); - all.add(new TCNameToken(node.location, "?", "?")); // Not state, but assumed to access state. + all.add(EVERYTHING); // Not state, but assumed to access state. return all; } @@ -142,4 +140,55 @@ public TCNameSet caseStatement(POStatement node, Boolean updates) { return newCollection(); } + + /** + * Identify the state names that are updated by a given state designator. + */ + private TCNameSet designatorUpdates(POStateDesignator sd) + { + TCNameSet all = newCollection(); + + if (sd instanceof POIdentifierDesignator) + { + POIdentifierDesignator id = (POIdentifierDesignator)sd; + all.add(id.name); + } + else if (sd instanceof POFieldDesignator) + { + POFieldDesignator fd = (POFieldDesignator)sd; + all.addAll(designatorUpdates(fd.object)); + } + else if (sd instanceof POMapSeqDesignator) + { + POMapSeqDesignator msd = (POMapSeqDesignator)sd; + all.addAll(designatorUpdates(msd.mapseq)); + } + + return all; + } + + /** + * Identify the names that are read by a given state designator. + */ + private TCNameSet designatorReads(POStateDesignator sd) + { + if (sd instanceof POIdentifierDesignator) + { + return newCollection(); + } + else if (sd instanceof POFieldDesignator) + { + POFieldDesignator fd = (POFieldDesignator)sd; + return designatorReads(fd.object); + } + else if (sd instanceof POMapSeqDesignator) + { + POMapSeqDesignator msd = (POMapSeqDesignator)sd; + TCNameSet all = designatorReads(msd.mapseq); + all.addAll(visitorSet.applyExpressionVisitor(msd.exp, false)); + return all; + } + + return newCollection(); + } } From 84458efb8722a2f087aa9551634878b837509f2e Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Sun, 20 Oct 2024 10:57:44 +0100 Subject: [PATCH 3/9] Remove reads/updatesState on PODefinitions --- .../vdmj/po/definitions/PODefinition.java | 16 ---------------- .../POExplicitOperationDefinition.java | 12 ------------ .../POImplicitOperationDefinition.java | 12 ------------ 3 files changed, 40 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinition.java index 715a35bd8..3c228ed98 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinition.java @@ -130,22 +130,6 @@ public final TCNameList getVariableNames() list.addAll(apply(new POGetVariableNamesVisitor(), null)); return list; } - - /** - * True, if the definition contains executable statements that update state. - */ - public boolean updatesState() - { - return false; - } - - /** - * True, if the definition contains executable statements that read state. - */ - public boolean readsState() - { - return false; - } /** * Return the static type of the definition. For example, the type of a 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 00b8db519..f3f5b5074 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 @@ -217,18 +217,6 @@ public POPatternListList getParamPatternList() list.add(parameterPatterns); return list; } - - @Override - public boolean updatesState() - { - return body.updatesState(); - } - - @Override - public boolean readsState() - { - return body.readsState(); - } @Override public R apply(PODefinitionVisitor visitor, S arg) 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 050655b17..cbbb03632 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 @@ -272,18 +272,6 @@ public POPatternList getParamPatternList() return plist; } - - @Override - public boolean updatesState() - { - return body == null ? false : body.updatesState(); - } - - @Override - public boolean readsState() - { - return body == null ? false : body.readsState(); - } @Override public R apply(PODefinitionVisitor visitor, S arg) From 05fe15231cdcc0ff71c60aeec12a9018b7c0c05a Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Sun, 20 Oct 2024 11:16:47 +0100 Subject: [PATCH 4/9] Improve some POG parse/check error messages --- vdmj/documentation/MESSAGES | 4 +++- .../main/java/com/fujitsu/vdmj/pog/ProofObligationList.java | 6 +++--- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/vdmj/documentation/MESSAGES b/vdmj/documentation/MESSAGES index b90a69b26..2012f206e 100644 --- a/vdmj/documentation/MESSAGES +++ b/vdmj/documentation/MESSAGES @@ -400,12 +400,14 @@ as the expected and actual values. 2327, "Type set1 is not available in classic" 2328, "Sequence binds are not available in classic" 2329, "Duplicate keyword" -2330, "Tokens found after expression at " +2330, "POG: Tokens found after obligation at " 2331, "Expecting inv, eq or ord clause" 2332, "Duplicate inv clause" 2333, "Type eq/ord clauses not available in classic" 2334, "Failed to instantiate ASTAnnotation" 2335, "Maximal '!' not allowed here" +2336, "POG: Obligation is not boolean?" +2337, "POG Obligation has type errors?" 3000, "Expression does not match declared type" 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 92d583b26..137b91368 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java @@ -200,7 +200,7 @@ private void typeCheck(ProofObligation obligation, String mname, Environment env if (!end.is(Token.EOF)) { - throw new ParserException(2330, "Tokens found after expression at " + end, LexLocation.ANY, 0); + throw new ParserException(2330, "POG: Tokens found after obligation at " + end, LexLocation.ANY, 0); } TCExpression tcexp = ClassMapper.getInstance(TCNode.MAPPINGS).convertLocal(ast); @@ -210,7 +210,7 @@ private void typeCheck(ProofObligation obligation, String mname, Environment env if (!potype.isType(TCBooleanType.class, obligation.location)) { - throw new ParserException(2330, "PO is not boolean?", obligation.location, 0); + throw new ParserException(2336, "POG: Obligation is not boolean?", obligation.location, 0); } // Weed out errors that we can cope with @@ -245,7 +245,7 @@ private void typeCheck(ProofObligation obligation, String mname, Environment env if (TypeChecker.getErrorCount() > 0) { - throw new ParserException(2330, "PO has type errors?", obligation.location, 0); + throw new ParserException(2337, "POG Obligation has type errors?", obligation.location, 0); } obligation.setCheckedExpression(tcexp); From 40831a5a290a89b34c1b4033d756870f43b37711 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Tue, 22 Oct 2024 17:25:06 +0100 Subject: [PATCH 5/9] Improve operation POs with dcl blocks --- .../vdmj/po/definitions/PODefinitionList.java | 4 +- .../vdmj/po/expressions/PODefExpression.java | 3 +- .../po/expressions/POLetDefExpression.java | 3 +- .../po/statements/POAssignmentStatement.java | 11 ++- .../vdmj/po/statements/POBlockStatement.java | 20 +++--- .../po/statements/POCallObjectStatement.java | 3 +- .../vdmj/po/statements/POCallStatement.java | 3 +- .../vdmj/po/statements/PODefStatement.java | 2 +- .../vdmj/po/statements/POForAllStatement.java | 8 +-- .../po/statements/POForIndexStatement.java | 7 +- .../statements/POForPatternBindStatement.java | 8 +-- .../vdmj/po/statements/POLetDefStatement.java | 2 +- .../com/fujitsu/vdmj/pog/PODclContext.java | 71 +++++++++++++++++++ .../java/com/fujitsu/vdmj/pog/POGState.java | 63 ++++++++++++---- .../com/fujitsu/vdmj/pog/POGStateList.java | 5 +- .../com/fujitsu/vdmj/pog/ProofObligation.java | 1 - .../fujitsu/vdmj/pog/ProofObligationList.java | 6 +- .../java/com/fujitsu/vdmj/junit/PogTest.java | 4 +- 18 files changed, 162 insertions(+), 62 deletions(-) create mode 100644 vdmj/src/main/java/com/fujitsu/vdmj/pog/PODclContext.java diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinitionList.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinitionList.java index 75a21e371..35e75f908 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinitionList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinitionList.java @@ -110,7 +110,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog * one. This is used in let/def expressions, where definitions can depend on * earlier definitions in the same expression. */ - public ProofObligationList getDefProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getDefProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList obligations = new ProofObligationList(); int count = 0; @@ -121,7 +121,7 @@ public ProofObligationList getDefProofObligations(POContextStack ctxt, Environme count++; ctxt.push(new PONameContext(d.getVariableNames())); - obligations.addAll(d.getProofObligations(ctxt, env)); + obligations.addAll(d.getProofObligations(ctxt, pogState, env)); ctxt.pop(); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PODefExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PODefExpression.java index 3116dcf21..6dea830cd 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PODefExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PODefExpression.java @@ -28,6 +28,7 @@ import com.fujitsu.vdmj.po.definitions.PODefinitionList; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.POLetDefContext; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -51,7 +52,7 @@ public String toString() @Override public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) { - ProofObligationList obligations = localDefs.getDefProofObligations(ctxt, env); + ProofObligationList obligations = localDefs.getDefProofObligations(ctxt, new POGState(), env); ctxt.push(new POLetDefContext(this.localDefs)); obligations.addAll(expression.getProofObligations(ctxt, env)); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POLetDefExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POLetDefExpression.java index 07c926db2..07626385b 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POLetDefExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POLetDefExpression.java @@ -28,6 +28,7 @@ import com.fujitsu.vdmj.po.definitions.PODefinitionList; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.POLetDefContext; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -55,7 +56,7 @@ public String toString() @Override public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) { - ProofObligationList obligations = localDefs.getDefProofObligations(ctxt, env); + ProofObligationList obligations = localDefs.getDefProofObligations(ctxt, new POGState(), env); ctxt.push(new POLetDefContext(this.localDefs)); // See bug #6 obligations.addAll(expression.getProofObligations(ctxt, env)); ctxt.pop(); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAssignmentStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAssignmentStatement.java index f6d43966b..a9d7e201d 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAssignmentStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAssignmentStatement.java @@ -28,12 +28,15 @@ import com.fujitsu.vdmj.po.definitions.POClassDefinition; import com.fujitsu.vdmj.po.definitions.POStateDefinition; import com.fujitsu.vdmj.po.expressions.POExpression; +import com.fujitsu.vdmj.po.statements.visitors.POStatementStateFinder; import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor; import com.fujitsu.vdmj.pog.POContextStack; import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.StateInvariantObligation; import com.fujitsu.vdmj.pog.SubTypeObligation; +import com.fujitsu.vdmj.tc.lex.TCNameSet; +import com.fujitsu.vdmj.tc.lex.TCNameToken; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.typechecker.Environment; import com.fujitsu.vdmj.typechecker.TypeComparator; @@ -85,7 +88,13 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog obligations.addAll(target.getProofObligations(ctxt)); obligations.addAll(exp.getProofObligations(ctxt, env)); obligations.stateUpdate(pogState, exp); - pogState.didUpdateState(true); + + TCNameSet updates = this.apply(new POStatementStateFinder(), true); + + for (TCNameToken update: updates) + { + pogState.didUpdateState(update); + } if (!TypeComparator.isSubType(ctxt.checkType(exp, expType), targetType)) { 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 c8c62745d..6eaab6b3c 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 @@ -25,12 +25,13 @@ package com.fujitsu.vdmj.po.statements; import com.fujitsu.vdmj.lex.LexLocation; +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.statements.visitors.POStatementVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.PODclContext; import com.fujitsu.vdmj.pog.POGState; -import com.fujitsu.vdmj.pog.POScopeContext; -import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -50,16 +51,19 @@ public POBlockStatement(LexLocation location, PODefinitionList assignmentDefs, P public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList obligations = assignmentDefs.getProofObligations(ctxt, pogState, env); - - ctxt.push(new POScopeContext()); - obligations.addAll(super.getProofObligations(ctxt, pogState, env)); - ctxt.pop(); - if (!assignmentDefs.isEmpty()) + POGState dclState = pogState.getLink(); + + for (PODefinition dcl: assignmentDefs) { - obligations.markUnchecked(ProofObligation.DCL_STATEMENT); + POAssignmentDefinition adef = (POAssignmentDefinition)dcl; + dclState.addDclState(adef.name); } + ctxt.push(new PODclContext(assignmentDefs)); + obligations.addAll(super.getProofObligations(ctxt, dclState, env)); + ctxt.pop(); + return obligations; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallObjectStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallObjectStatement.java index e0cad3b6e..44ef22bb0 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallObjectStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallObjectStatement.java @@ -76,8 +76,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog } // We have to assume the operation call accesses state - pogState.didReadState(true); - pogState.didUpdateState(true); + pogState.didUpdateState(); return obligations; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallStatement.java index 3f73e9970..a4be51307 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallStatement.java @@ -64,8 +64,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog } // We have to assume the operation call accesses state - pogState.didReadState(true); - pogState.didUpdateState(true); + pogState.didUpdateState(); return obligations; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/PODefStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/PODefStatement.java index 7e919ee01..04d6653ce 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/PODefStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/PODefStatement.java @@ -56,7 +56,7 @@ public String toString() @Override public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList obligations = equalsDefs.getDefProofObligations(ctxt, env); + ProofObligationList obligations = equalsDefs.getDefProofObligations(ctxt, pogState, env); ctxt.push(new POLetDefContext(equalsDefs)); obligations.addAll(statement.getProofObligations(ctxt, pogState, env)); 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 99a77f4bc..83feb5d96 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 @@ -63,13 +63,9 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog obligations.stateUpdate(pogState, set); ProofObligationList loops = statement.getProofObligations(ctxt, pogState, env); - - if (statement.updatesState()) - { - loops.markUnchecked(ProofObligation.LOOP_STATEMENT); - } - + loops.markUnchecked(ProofObligation.LOOP_STATEMENT); obligations.addAll(loops); + 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 f97947463..6c0f40b78 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 @@ -77,12 +77,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog ctxt.push(new POScopeContext()); ProofObligationList loops = statement.getProofObligations(ctxt, pogState, env); - - if (statement.updatesState()) - { - loops.markUnchecked(ProofObligation.LOOP_STATEMENT); - } - + loops.markUnchecked(ProofObligation.LOOP_STATEMENT); obligations.addAll(loops); ctxt.pop(); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForPatternBindStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForPatternBindStatement.java index 47a8fb4a2..9dd1f4393 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForPatternBindStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForPatternBindStatement.java @@ -99,13 +99,9 @@ else if (patternBind.bind instanceof POSeqBind) } ProofObligationList loops = statement.getProofObligations(ctxt, pogState, env); - - if (statement.updatesState()) - { - loops.markUnchecked(ProofObligation.LOOP_STATEMENT); - } - + loops.markUnchecked(ProofObligation.LOOP_STATEMENT); list.addAll(loops); + return list; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POLetDefStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POLetDefStatement.java index f0df04d3b..dbf34ae7d 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POLetDefStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POLetDefStatement.java @@ -55,7 +55,7 @@ public String toString() @Override public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList obligations = localDefs.getDefProofObligations(ctxt, env); + ProofObligationList obligations = localDefs.getDefProofObligations(ctxt, pogState, env); ctxt.push(new POLetDefContext(this.localDefs)); obligations.addAll(statement.getProofObligations(ctxt, pogState, env)); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/PODclContext.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/PODclContext.java new file mode 100644 index 000000000..9dd156146 --- /dev/null +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/PODclContext.java @@ -0,0 +1,71 @@ +/******************************************************************************* + * + * 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; + +import com.fujitsu.vdmj.po.definitions.POAssignmentDefinition; +import com.fujitsu.vdmj.po.definitions.PODefinition; +import com.fujitsu.vdmj.po.definitions.PODefinitionList; + +public class PODclContext extends POContext +{ + public final PODefinitionList assignmentDefs; + + public PODclContext(PODefinitionList assignmentDefs) + { + this.assignmentDefs = assignmentDefs; + } + + @Override + public boolean isScopeBoundary() + { + return true; + } + + @Override + public String getSource() + { + StringBuilder sb = new StringBuilder(); + + if (!assignmentDefs.isEmpty()) + { + sb.append("let "); + String sep = ""; + + for (PODefinition def: assignmentDefs) + { + sb.append(sep); + POAssignmentDefinition adef = (POAssignmentDefinition)def; + sb.append(adef.name); + sb.append(" = "); + sb.append(adef.expression); + sep = ", "; + } + + sb.append(" in"); + } + + return sb.toString(); + } +} diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POGState.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POGState.java index 26529f422..adc89f5c7 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POGState.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POGState.java @@ -23,6 +23,10 @@ ******************************************************************************/ package com.fujitsu.vdmj.pog; +import com.fujitsu.vdmj.tc.lex.TCNameList; +import com.fujitsu.vdmj.tc.lex.TCNameToken; +import com.fujitsu.vdmj.util.Utils; + /** * A class to hold state information for POG of statements, which involve potentially * changing state variables. @@ -30,49 +34,80 @@ public class POGState { private boolean hasUpdatedState; - private boolean hasReadState; + private POGState outerState; + private TCNameList locals; public POGState() { hasUpdatedState = false; - hasReadState = false; + outerState = null; + locals = new TCNameList(); } - private POGState(boolean hasUpdatedState, boolean hasReadState) + private POGState(boolean hasUpdatedState, POGState outerState) { this.hasUpdatedState = hasUpdatedState; - this.hasReadState = hasReadState; + this.outerState = outerState; + this.locals = new TCNameList(); } @Override public String toString() { - return (hasUpdatedState ? "has" : "has not") + " updated state; " + - (hasReadState ? "has" : "has not") + " read state"; + return (hasUpdatedState ? "has" : "has not") + " updated state" + + (locals.isEmpty() ? "" : Utils.listToString("(locals ", locals, ", ", ")")); } public POGState getCopy() { - return new POGState(hasUpdatedState, hasReadState); + return new POGState(hasUpdatedState, outerState); + } + + public POGState getLink() + { + return new POGState(false, this); } public boolean hasUpdatedState() { - return hasUpdatedState; + return hasUpdatedState || (outerState != null && outerState.hasUpdatedState()); + } + + public void setUpdateState(boolean updatedState) + { + hasUpdatedState = hasUpdatedState || updatedState; } - public boolean hasReadState() + public void didUpdateState() // Used by call statements { - return hasReadState; + if (outerState != null) + { + outerState.didUpdateState(); + } + else + { + hasUpdatedState = true; // Module level + } } - public void didUpdateState(boolean flag) + public void didUpdateState(TCNameToken name) { - hasUpdatedState = hasUpdatedState || flag; + if (locals.contains(name)) + { + hasUpdatedState = true; // A local dcl update + } + else if (outerState != null) + { + outerState.didUpdateState(name); // May be an outer* local + } + else + { + hasUpdatedState = true; // A module state update + } } - public void didReadState(boolean flag) + public void addDclState(TCNameToken name) { - hasReadState = hasReadState || flag; + locals.add(name); } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POGStateList.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POGStateList.java index c036d20e3..31683bd92 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POGStateList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POGStateList.java @@ -49,15 +49,12 @@ public POGState addCopy(POGState parent) public void combineInto(POGState parent) { boolean hasUpdatedState = false; - boolean hasReadState = false; for (POGState state: this) { hasUpdatedState = hasUpdatedState || state.hasUpdatedState(); - hasReadState = hasReadState || state.hasReadState(); } - parent.didUpdateState(hasUpdatedState); - parent.didReadState(hasReadState); + parent.setUpdateState(hasUpdatedState); } } 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 7f93b7c0c..c5fc1f900 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java @@ -59,7 +59,6 @@ abstract public class ProofObligation implements Comparable public static final String REQUIRES_VDM10 = "Obligation requires VDM10"; public static final String BODY_UPDATES_STATE = "Operation body updates state"; public static final String LOOP_STATEMENT = "Loop modifies state"; - 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; 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 137b91368..c8336ab58 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java @@ -275,8 +275,8 @@ public ProofObligationList markUnchecked(String message) } /** - * Update the obligations in this list because of the current POGState, and then update - * the POGState to account for the state read/updates in expression. + * Update the obligations in this list because of the current POGState and the state read + * by the expression. */ public void stateUpdate(POGState pstate, POExpression expression) { @@ -286,7 +286,5 @@ public void stateUpdate(POGState pstate, POExpression expression) { markUnchecked(ProofObligation.HAS_UPDATED_STATE); } - - pstate.didReadState(readsState); } } diff --git a/vdmj/src/test/java/com/fujitsu/vdmj/junit/PogTest.java b/vdmj/src/test/java/com/fujitsu/vdmj/junit/PogTest.java index c5e3426ea..ebaaa92db 100644 --- a/vdmj/src/test/java/com/fujitsu/vdmj/junit/PogTest.java +++ b/vdmj/src/test/java/com/fujitsu/vdmj/junit/PogTest.java @@ -147,8 +147,8 @@ protected void tearDown() throws Exception /* 81 */ "(forall i:int, obj_A(iv |-> 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 &\n while (x > 0) do ...)\n", - /* 85 */ "(forall obj_A(iv |-> iv):A &\n let iv = (iv + 1) in (iv < 10))\n", + /* 84 */ "(forall obj_A(iv |-> iv):A &\n (let x = 10 in\n while (x > 0) do ...))\n", + /* 85 */ "(forall obj_A(iv |-> iv):A &\n (let x = 10 in\n let iv = (iv + 1) in (iv < 10)))\n", }; public void testPOG() throws Exception From 973f70cf99efaf683e8c3363ed25872d28f3cf98 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Tue, 22 Oct 2024 22:09:32 +0100 Subject: [PATCH 6/9] Add POGState to all POExpressions --- .../po/annotations/POAnnotatedExpression.java | 5 +++-- .../definitions/POAssignmentDefinition.java | 2 +- .../po/definitions/POClassDefinition.java | 10 ++++++++-- .../POClassInvariantDefinition.java | 3 ++- .../vdmj/po/definitions/POClassList.java | 3 ++- .../vdmj/po/definitions/PODefinition.java | 12 +++-------- .../vdmj/po/definitions/PODefinitionList.java | 20 ------------------- .../po/definitions/POEqualsDefinition.java | 9 +++++---- .../POExplicitFunctionDefinition.java | 11 +++++----- .../POExplicitOperationDefinition.java | 14 ++++++------- .../POImplicitFunctionDefinition.java | 11 +++++----- .../POImplicitOperationDefinition.java | 14 ++++++------- .../po/definitions/POPerSyncDefinition.java | 5 +++-- .../po/definitions/POQualifiedDefinition.java | 5 +++-- .../po/definitions/POStateDefinition.java | 7 ++++--- .../vdmj/po/definitions/POTypeDefinition.java | 9 +++++---- .../po/definitions/POValueDefinition.java | 6 ++++-- .../vdmj/po/expressions/POAndExpression.java | 7 ++++--- .../po/expressions/POApplyExpression.java | 12 ++++++++--- .../po/expressions/POBinaryExpression.java | 7 ++++--- .../POBooleanBinaryExpression.java | 5 +++-- .../po/expressions/POCaseAlternative.java | 5 +++-- .../po/expressions/POCasesExpression.java | 9 +++++---- .../vdmj/po/expressions/POCompExpression.java | 3 ++- .../vdmj/po/expressions/PODefExpression.java | 6 +++--- .../PODistIntersectExpression.java | 5 +++-- .../po/expressions/PODistMergeExpression.java | 3 ++- .../vdmj/po/expressions/PODivExpression.java | 5 +++-- .../po/expressions/PODivideExpression.java | 5 +++-- .../po/expressions/POElementsExpression.java | 5 +++-- .../po/expressions/POElseIfExpression.java | 7 ++++--- .../po/expressions/POExists1Expression.java | 7 ++++--- .../po/expressions/POExistsExpression.java | 7 ++++--- .../vdmj/po/expressions/POExpression.java | 4 +++- .../vdmj/po/expressions/POExpressionList.java | 5 +++-- .../po/expressions/POFieldExpression.java | 5 +++-- .../expressions/POFieldNumberExpression.java | 5 +++-- .../po/expressions/POForAllExpression.java | 7 ++++--- .../POFuncInstantiationExpression.java | 5 +++-- .../expressions/POGreaterEqualExpression.java | 5 +++-- .../po/expressions/POGreaterExpression.java | 5 +++-- .../vdmj/po/expressions/POHeadExpression.java | 5 +++-- .../vdmj/po/expressions/POIfExpression.java | 11 +++++----- .../po/expressions/POImpliesExpression.java | 7 ++++--- .../vdmj/po/expressions/POIotaExpression.java | 7 ++++--- .../vdmj/po/expressions/POIsExpression.java | 5 +++-- .../POIsOfBaseClassExpression.java | 5 +++-- .../po/expressions/POIsOfClassExpression.java | 5 +++-- .../po/expressions/POLambdaExpression.java | 7 ++++--- .../po/expressions/POLessEqualExpression.java | 5 +++-- .../vdmj/po/expressions/POLessExpression.java | 5 +++-- .../po/expressions/POLetBeStExpression.java | 9 +++++---- .../po/expressions/POLetDefExpression.java | 7 ++++--- .../po/expressions/POMapCompExpression.java | 9 +++++---- .../po/expressions/POMapEnumExpression.java | 5 +++-- .../expressions/POMapInverseExpression.java | 5 +++-- .../po/expressions/POMapUnionExpression.java | 5 +++-- .../po/expressions/POMapletExpression.java | 7 ++++--- .../po/expressions/POMkBasicExpression.java | 5 +++-- .../po/expressions/POMkTypeExpression.java | 5 +++-- .../vdmj/po/expressions/POMuExpression.java | 7 ++++--- .../po/expressions/PONarrowExpression.java | 5 +++-- .../vdmj/po/expressions/PONewExpression.java | 5 +++-- .../PONumericBinaryExpression.java | 11 +++++----- .../vdmj/po/expressions/POOrExpression.java | 7 ++++--- .../po/expressions/POPlusPlusExpression.java | 5 +++-- .../POSameBaseClassExpression.java | 7 ++++--- .../po/expressions/POSameClassExpression.java | 7 ++++--- .../po/expressions/POSeqCompExpression.java | 9 +++++---- .../po/expressions/POSeqEnumExpression.java | 5 +++-- .../po/expressions/POSetCompExpression.java | 9 +++++---- .../po/expressions/POSetEnumExpression.java | 5 +++-- .../po/expressions/POSetRangeExpression.java | 7 ++++--- .../po/expressions/POStarStarExpression.java | 3 ++- .../po/expressions/POSubseqExpression.java | 9 +++++---- .../vdmj/po/expressions/POTailExpression.java | 5 +++-- .../po/expressions/POTupleExpression.java | 5 +++-- .../po/expressions/POUnaryExpression.java | 5 +++-- .../visitors/POExpressionStateFinder.java | 19 ++++++++++++++++++ .../com/fujitsu/vdmj/po/modules/POModule.java | 11 +++++++++- .../com/fujitsu/vdmj/po/patterns/POBind.java | 3 ++- .../vdmj/po/patterns/POMultipleBind.java | 3 ++- .../vdmj/po/patterns/POMultipleSeqBind.java | 5 +++-- .../vdmj/po/patterns/POMultipleSetBind.java | 5 +++-- .../vdmj/po/patterns/POMultipleTypeBind.java | 3 ++- .../fujitsu/vdmj/po/patterns/POSeqBind.java | 5 +++-- .../fujitsu/vdmj/po/patterns/POSetBind.java | 5 +++-- .../fujitsu/vdmj/po/patterns/POTypeBind.java | 3 ++- .../po/statements/POAssignmentStatement.java | 2 +- .../po/statements/POCallObjectStatement.java | 2 +- .../vdmj/po/statements/POCallStatement.java | 2 +- .../vdmj/po/statements/POExitStatement.java | 2 +- .../vdmj/po/statements/POForAllStatement.java | 2 +- .../po/statements/POForIndexStatement.java | 6 +++--- .../statements/POForPatternBindStatement.java | 6 +++--- .../vdmj/po/statements/POIfStatement.java | 4 ++-- .../po/statements/POLetBeStStatement.java | 4 ++-- .../vdmj/po/statements/POReturnStatement.java | 2 +- .../statements/POSpecificationStatement.java | 8 ++++---- .../vdmj/po/statements/POStartStatement.java | 2 +- .../vdmj/po/statements/POStopStatement.java | 2 +- .../po/statements/POTixeStmtAlternative.java | 4 ++-- .../vdmj/po/statements/POTrapStatement.java | 4 ++-- .../vdmj/po/statements/POWhileStatement.java | 2 +- .../fujitsu/vdmj/pog/ProofObligationList.java | 7 ++++--- 105 files changed, 367 insertions(+), 276 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedExpression.java index 72da7110c..c69fdda17 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedExpression.java @@ -28,6 +28,7 @@ import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -53,10 +54,10 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { annotation.poBefore(this, ctxt); - ProofObligationList obligations = expression.getProofObligations(ctxt, env); + ProofObligationList obligations = expression.getProofObligations(ctxt, pogState, env); annotation.poAfter(this, obligations, ctxt); return obligations; } 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 105e2c48b..818aedd30 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 @@ -70,7 +70,7 @@ public TCType getType() public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList obligations = new ProofObligationList(); - obligations.addAll(expression.getProofObligations(ctxt, env)); + obligations.addAll(expression.getProofObligations(ctxt, pogState, env)); obligations.stateUpdate(pogState, expression); if (!TypeComparator.isSubType(ctxt.checkType(expression, expType), type)) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassDefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassDefinition.java index cac218ad7..69762ff46 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassDefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassDefinition.java @@ -28,6 +28,7 @@ import com.fujitsu.vdmj.po.definitions.visitors.PODefinitionVisitor; import com.fujitsu.vdmj.po.statements.POClassInvariantStatement; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.definitions.TCClassDefinition; import com.fujitsu.vdmj.tc.lex.TCNameToken; @@ -172,14 +173,19 @@ public boolean hasNew() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment publicEnv) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment publicEnv) { ProofObligationList list = (annotations != null) ? annotations.poBefore(this) : new ProofObligationList(); Environment env = new PrivateClassEnvironment(tcdef, publicEnv); Environment local = new FlatEnvironment(tcdef.getSelfDefinition(), env); - list.addAll(definitions.getProofObligations(ctxt, local)); + + for (PODefinition def: definitions) + { + list.addAll(def.getProofObligations(new POContextStack(), new POGState(), local)); + } + list.typeCheck(tcdef.name, local); if (annotations != null) annotations.poAfter(this, list); 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 de41939a1..b1b7eee80 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,6 +27,7 @@ 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.POGState; import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.StateInvariantObligation; @@ -63,7 +64,7 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList list = new ProofObligationList(); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassList.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassList.java index e7b27b508..68b642c04 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassList.java @@ -26,6 +26,7 @@ import com.fujitsu.vdmj.po.POMappedList; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.definitions.TCClassDefinition; import com.fujitsu.vdmj.tc.definitions.TCClassList; @@ -72,7 +73,7 @@ public ProofObligationList getProofObligations() for (POClassDefinition c: this) { - obligations.addAll(c.getProofObligations(new POContextStack(), new PublicClassEnvironment(tcclasses))); + obligations.addAll(c.getProofObligations(new POContextStack(), new POGState(), new PublicClassEnvironment(tcclasses))); } return obligations; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinition.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinition.java index 3c228ed98..eac306047 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinition.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinition.java @@ -146,21 +146,15 @@ public final TCNameList getVariableNames() abstract public TCType getType(); /** - * Get a list of proof obligations for the definition. The second method is used - * to track the POG state for updates to state variables, which is only used - * by a few definition types (eg. POAssignmentDefinitions). + * Get a list of proof obligations for the definition. * * @param ctxt The call context. + * @param pogState Tracks updates to state in operations. * @return A list of POs. */ - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) - { - return new ProofObligationList(); - } - public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return getProofObligations(ctxt, env); // Default to stateless version + return new ProofObligationList(); } /** diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinitionList.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinitionList.java index 35e75f908..041d32956 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinitionList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinitionList.java @@ -28,7 +28,6 @@ import com.fujitsu.vdmj.pog.POContextStack; import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.POLetDefContext; -import com.fujitsu.vdmj.pog.PONameContext; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.definitions.TCDefinition; import com.fujitsu.vdmj.tc.definitions.TCDefinitionList; @@ -73,23 +72,6 @@ public String toString() return sb.toString(); } - /** - * Get the proof obligations from every definition in the list. - */ - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) - { - ProofObligationList obligations = new ProofObligationList(); - - for (PODefinition d: this) - { - ctxt.push(new PONameContext(d.getVariableNames())); - obligations.addAll(d.getProofObligations(ctxt, env)); - ctxt.pop(); - } - - return obligations; - } - /** * Get the proof obligations from every definition in the list and track POGState. */ @@ -120,9 +102,7 @@ public ProofObligationList getDefProofObligations(POContextStack ctxt, POGState ctxt.push(new POLetDefContext(d)); // In scope for recursive or total obligations count++; - ctxt.push(new PONameContext(d.getVariableNames())); obligations.addAll(d.getProofObligations(ctxt, pogState, env)); - ctxt.pop(); } for (int i=0; i " + result; } - public ProofObligationList getProofObligations(POContextStack ctxt, TCType type, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, TCType type, Environment env) { ProofObligationList obligations = new ProofObligationList(); ctxt.push(new POCaseContext(pattern, type, cexp)); - obligations.addAll(result.getProofObligations(ctxt, env)); + obligations.addAll(result.getProofObligations(ctxt, pogState, env)); ctxt.pop(); ctxt.push(new PONotCaseContext(pattern, type, cexp)); 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 8c4e8c737..f1c740003 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.POGState; import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.lex.TCNameList; @@ -63,9 +64,9 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList obligations = exp.getProofObligations(ctxt, env); + ProofObligationList obligations = exp.getProofObligations(ctxt, pogState, env); boolean hasIgnore = false; TCNameList hidden = new TCNameList(); @@ -81,12 +82,12 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment hidden.addAll(alt.pattern.getHiddenVariables()); // cumulative // PONotCaseContext pushed by the POCaseAlternative... - _obligations.addAll(alt.getProofObligations(ctxt, expType, env)); + _obligations.addAll(alt.getProofObligations(ctxt, pogState, expType, env)); } if (others != null) { - _obligations.addAll(others.getProofObligations(ctxt, env)); + _obligations.addAll(others.getProofObligations(ctxt, pogState, env)); } for (int i=0; i for (POElseIfExpression exp: elseList) { - obligations.addAll(exp.getProofObligations(ctxt, env)); + obligations.addAll(exp.getProofObligations(ctxt, pogState, env)); ctxt.push(new PONotImpliesContext(exp.elseIfExp)); } - obligations.addAll(elseExp.getProofObligations(ctxt, env)); + obligations.addAll(elseExp.getProofObligations(ctxt, pogState, env)); for (int i=0; i 1) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMapInverseExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMapInverseExpression.java index 3d337f9c5..e92d4ba43 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMapInverseExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMapInverseExpression.java @@ -28,6 +28,7 @@ import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.InvariantObligation; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCMapType; import com.fujitsu.vdmj.tc.types.TCTypeQualifier; @@ -51,9 +52,9 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList list = super.getProofObligations(ctxt, env); + ProofObligationList list = super.getProofObligations(ctxt, pogState, env); if (!type.empty) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMapUnionExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMapUnionExpression.java index f3146b087..43a9d1d4c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMapUnionExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMapUnionExpression.java @@ -28,6 +28,7 @@ import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.MapCompatibleObligation; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.tc.types.TCTypeQualifier; @@ -44,9 +45,9 @@ public POMapUnionExpression(POExpression left, LexToken op, POExpression right, } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList obligations = super.getProofObligations(ctxt, env); + ProofObligationList obligations = super.getProofObligations(ctxt, pogState, env); obligations.add(new MapCompatibleObligation(left, right, ctxt)); return obligations; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMapletExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMapletExpression.java index 4d2ecd5f2..c224c4f25 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMapletExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMapletExpression.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.PONode; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -51,10 +52,10 @@ public String toString() return left + " |-> " + right; } - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList list = left.getProofObligations(ctxt, env); - list.addAll(right.getProofObligations(ctxt, env)); + ProofObligationList list = left.getProofObligations(ctxt, pogState, env); + list.addAll(right.getProofObligations(ctxt, pogState, env)); return list; } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMkBasicExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMkBasicExpression.java index 6ef946d8f..26848bd39 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMkBasicExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMkBasicExpression.java @@ -26,6 +26,7 @@ import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.typechecker.Environment; @@ -50,9 +51,9 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return arg.getProofObligations(ctxt, env); + return arg.getProofObligations(ctxt, pogState, env); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMkTypeExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMkTypeExpression.java index 118073bb4..13514a9b0 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMkTypeExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMkTypeExpression.java @@ -28,6 +28,7 @@ import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.SubTypeObligation; import com.fujitsu.vdmj.tc.lex.TCNameToken; @@ -64,9 +65,9 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList list = args.getProofObligations(ctxt, env); + ProofObligationList list = args.getProofObligations(ctxt, pogState, env); Iterator it = argTypes.iterator(); int i = 0; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMuExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMuExpression.java index 40b71b3e7..b20e3f925 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMuExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POMuExpression.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.SubTypeObligation; import com.fujitsu.vdmj.tc.types.TCField; @@ -62,14 +63,14 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList list = record.getProofObligations(ctxt, env); + ProofObligationList list = record.getProofObligations(ctxt, pogState, env); int i = 0; for (PORecordModifier rm: modifiers) { - list.addAll(rm.value.getProofObligations(ctxt, env)); + list.addAll(rm.value.getProofObligations(ctxt, pogState, env)); TCField f = recordType.findField(rm.tag.getName()); TCType mtype = modTypes.get(i++); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PONarrowExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PONarrowExpression.java index 0ff5d6c70..41dabec0b 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PONarrowExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PONarrowExpression.java @@ -28,6 +28,7 @@ import com.fujitsu.vdmj.po.definitions.PODefinition; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.SubTypeObligation; import com.fujitsu.vdmj.tc.lex.TCNameToken; @@ -62,7 +63,7 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList obligations = new ProofObligationList(); @@ -74,7 +75,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment obligations.add(new SubTypeObligation(test, expected, testtype, ctxt)); } - obligations.addAll(test.getProofObligations(ctxt, env)); + obligations.addAll(test.getProofObligations(ctxt, pogState, env)); return obligations; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PONewExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PONewExpression.java index 693e878b4..5e909df41 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PONewExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PONewExpression.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.lex.TCIdentifierToken; import com.fujitsu.vdmj.typechecker.Environment; @@ -52,9 +53,9 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return args.getProofObligations(ctxt, env); + return args.getProofObligations(ctxt, pogState, env); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PONumericBinaryExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PONumericBinaryExpression.java index 8b3d0b7f1..f4330bcb2 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PONumericBinaryExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/PONumericBinaryExpression.java @@ -28,6 +28,7 @@ import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.OrderedObligation; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.SubTypeObligation; import com.fujitsu.vdmj.tc.types.TCOptionalType; @@ -48,9 +49,9 @@ public PONumericBinaryExpression(POExpression left, LexToken op, POExpression ri } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList obligations = super.getProofObligations(ctxt, env); + ProofObligationList obligations = super.getProofObligations(ctxt, pogState, env); obligations.addAll(getNonNilObligations(ctxt)); return obligations; } @@ -80,11 +81,11 @@ private ProofObligationList getNonNilObligations(POContextStack ctxt) /** * Generate ordering obligations, as used by the comparison operators. */ - protected ProofObligationList getOrderedObligations(POContextStack ctxt, Environment env) + protected ProofObligationList getOrderedObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList obligations = getCommonOrderedObligations(ctxt); - obligations.addAll(left.getProofObligations(ctxt, env)); - obligations.addAll(right.getProofObligations(ctxt, env)); + obligations.addAll(left.getProofObligations(ctxt, pogState, env)); + obligations.addAll(right.getProofObligations(ctxt, pogState, env)); return obligations; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POOrExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POOrExpression.java index ce238a96d..3b8be8fac 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POOrExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POOrExpression.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.ast.lex.LexToken; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.PONotImpliesContext; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.SubTypeObligation; @@ -45,7 +46,7 @@ public POOrExpression(POExpression left, LexToken op, POExpression right, } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList obligations = new ProofObligationList(); @@ -63,10 +64,10 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment ctxt.pop(); } - obligations.addAll(left.getProofObligations(ctxt, env)); + obligations.addAll(left.getProofObligations(ctxt, pogState, env)); ctxt.push(new PONotImpliesContext(left)); - obligations.addAll(right.getProofObligations(ctxt, env)); + obligations.addAll(right.getProofObligations(ctxt, pogState, env)); ctxt.pop(); return obligations; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POPlusPlusExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POPlusPlusExpression.java index 43508d483..2ec0d4fa4 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POPlusPlusExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POPlusPlusExpression.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.ast.lex.LexToken; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.SeqModificationObligation; import com.fujitsu.vdmj.tc.types.TCType; @@ -44,9 +45,9 @@ public POPlusPlusExpression(POExpression left, LexToken op, POExpression right, } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList obligations = super.getProofObligations(ctxt, env); + ProofObligationList obligations = super.getProofObligations(ctxt, pogState, env); if (ltype.isSeq(location)) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSameBaseClassExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSameBaseClassExpression.java index db7483d31..f76cde39e 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSameBaseClassExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSameBaseClassExpression.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -45,10 +46,10 @@ public POSameBaseClassExpression(LexLocation start, POExpression left, POExpress } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList list = left.getProofObligations(ctxt, env); - list.addAll(right.getProofObligations(ctxt, env)); + ProofObligationList list = left.getProofObligations(ctxt, pogState, env); + list.addAll(right.getProofObligations(ctxt, pogState, env)); return list; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSameClassExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSameClassExpression.java index e4e728353..de3c0a0f1 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSameClassExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSameClassExpression.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -45,10 +46,10 @@ public POSameClassExpression(LexLocation start, POExpression left, POExpression } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList list = left.getProofObligations(ctxt, env); - list.addAll(right.getProofObligations(ctxt, env)); + ProofObligationList list = left.getProofObligations(ctxt, pogState, env); + list.addAll(right.getProofObligations(ctxt, pogState, env)); return list; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSeqCompExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSeqCompExpression.java index 4c5fcf37e..b88912c34 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSeqCompExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSeqCompExpression.java @@ -28,6 +28,7 @@ import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.po.patterns.POBind; import com.fujitsu.vdmj.pog.POForAllPredicateContext; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.POForAllContext; import com.fujitsu.vdmj.pog.POContextStack; import com.fujitsu.vdmj.pog.ProofObligationList; @@ -58,20 +59,20 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList obligations = new ProofObligationList(); ctxt.push(new POForAllPredicateContext(this)); - obligations.addAll(first.getProofObligations(ctxt, env)); + obligations.addAll(first.getProofObligations(ctxt, pogState, env)); ctxt.pop(); - obligations.addAll(bind.getProofObligations(ctxt, env)); + obligations.addAll(bind.getProofObligations(ctxt, pogState, env)); if (predicate != null) { ctxt.push(new POForAllContext(this)); - obligations.addAll(predicate.getProofObligations(ctxt, env)); + obligations.addAll(predicate.getProofObligations(ctxt, pogState, env)); obligations.addAll(checkUnionQualifiers(predicate, TCTypeQualifier.getBoolQualifier(), ctxt)); ctxt.pop(); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSeqEnumExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSeqEnumExpression.java index 6478625c3..1fc078afb 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSeqEnumExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSeqEnumExpression.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCTypeList; import com.fujitsu.vdmj.typechecker.Environment; @@ -52,9 +53,9 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return members.getProofObligations(ctxt, env); + return members.getProofObligations(ctxt, pogState, env); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSetCompExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSetCompExpression.java index 058517f80..428b14476 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSetCompExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSetCompExpression.java @@ -33,6 +33,7 @@ import com.fujitsu.vdmj.pog.POContextStack; import com.fujitsu.vdmj.pog.POForAllContext; import com.fujitsu.vdmj.pog.POForAllPredicateContext; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCSetType; import com.fujitsu.vdmj.tc.types.TCTypeQualifier; @@ -65,19 +66,19 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList obligations = new ProofObligationList(); ctxt.push(new POForAllPredicateContext(this)); - obligations.addAll(first.getProofObligations(ctxt, env)); + obligations.addAll(first.getProofObligations(ctxt, pogState, env)); ctxt.pop(); boolean finiteTest = false; for (POMultipleBind mb: bindings) { - obligations.addAll(mb.getProofObligations(ctxt, env)); + obligations.addAll(mb.getProofObligations(ctxt, pogState, env)); if (mb instanceof POMultipleTypeBind) { @@ -93,7 +94,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment if (predicate != null) { ctxt.push(new POForAllContext(this)); - obligations.addAll(predicate.getProofObligations(ctxt, env)); + obligations.addAll(predicate.getProofObligations(ctxt, pogState, env)); obligations.addAll(checkUnionQualifiers(predicate, TCTypeQualifier.getBoolQualifier(), ctxt)); ctxt.pop(); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSetEnumExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSetEnumExpression.java index 77ca4af99..4e4a06e11 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSetEnumExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSetEnumExpression.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCTypeList; import com.fujitsu.vdmj.typechecker.Environment; @@ -52,9 +53,9 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return members.getProofObligations(ctxt, env); + return members.getProofObligations(ctxt, pogState, env); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSetRangeExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSetRangeExpression.java index 34256bf24..a755c6369 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSetRangeExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSetRangeExpression.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.tc.types.TCTypeQualifier; @@ -57,10 +58,10 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList obligations = first.getProofObligations(ctxt, env); - obligations.addAll(last.getProofObligations(ctxt, env)); + ProofObligationList obligations = first.getProofObligations(ctxt, pogState, env); + obligations.addAll(last.getProofObligations(ctxt, pogState, env)); obligations.addAll(checkUnionQualifiers(first, TCTypeQualifier.getNumericQualifier(), ctxt)); obligations.addAll(checkUnionQualifiers(last, TCTypeQualifier.getNumericQualifier(), ctxt)); return obligations; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POStarStarExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POStarStarExpression.java index d34c85b24..e322ba25c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POStarStarExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POStarStarExpression.java @@ -29,6 +29,7 @@ import com.fujitsu.vdmj.pog.FuncIterationObligation; import com.fujitsu.vdmj.pog.MapIterationObligation; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.tc.types.TCTypeQualifier; @@ -45,7 +46,7 @@ public POStarStarExpression(POExpression left, LexToken op, POExpression right, } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { ProofObligationList obligations = new ProofObligationList(); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSubseqExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSubseqExpression.java index a355b5b09..9e2240cf1 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSubseqExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POSubseqExpression.java @@ -26,6 +26,7 @@ import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.tc.types.TCTypeQualifier; @@ -58,11 +59,11 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList list = seq.getProofObligations(ctxt, env); - list.addAll(from.getProofObligations(ctxt, env)); - list.addAll(to.getProofObligations(ctxt, env)); + ProofObligationList list = seq.getProofObligations(ctxt, pogState, env); + list.addAll(from.getProofObligations(ctxt, pogState, env)); + list.addAll(to.getProofObligations(ctxt, pogState, env)); list.addAll(checkUnionQualifiers(from, TCTypeQualifier.getNumericQualifier(), ctxt)); list.addAll(checkUnionQualifiers(to, TCTypeQualifier.getNumericQualifier(), ctxt)); return list; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POTailExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POTailExpression.java index 1a65c21da..0e298a472 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POTailExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POTailExpression.java @@ -28,6 +28,7 @@ import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.NonEmptySeqObligation; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCSeq1Type; import com.fujitsu.vdmj.tc.types.TCType; @@ -52,9 +53,9 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList obligations = super.getProofObligations(ctxt, env); + ProofObligationList obligations = super.getProofObligations(ctxt, pogState, env); if (!etype.isAlways(TCSeq1Type.class, location)) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POTupleExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POTupleExpression.java index 362d9d2fe..ca7f7d4c5 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POTupleExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POTupleExpression.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCTypeList; import com.fujitsu.vdmj.typechecker.Environment; @@ -52,9 +53,9 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return args.getProofObligations(ctxt, env); + return args.getProofObligations(ctxt, pogState, env); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POUnaryExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POUnaryExpression.java index 2b3830fa7..e73e3f3be 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POUnaryExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POUnaryExpression.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.pog.SubTypeObligation; import com.fujitsu.vdmj.tc.types.TCType; @@ -47,9 +48,9 @@ public POUnaryExpression(LexLocation location, POExpression exp) } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList list = exp.getProofObligations(ctxt, env); + ProofObligationList list = exp.getProofObligations(ctxt, pogState, env); if (exp.getExptype() != null && exp.getExptype().isUnion(location)) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/visitors/POExpressionStateFinder.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/visitors/POExpressionStateFinder.java index d5a1867bf..985c422b5 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/visitors/POExpressionStateFinder.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/visitors/POExpressionStateFinder.java @@ -25,10 +25,12 @@ package com.fujitsu.vdmj.po.expressions.visitors; import com.fujitsu.vdmj.po.POVisitorSet; +import com.fujitsu.vdmj.po.expressions.POApplyExpression; import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.po.expressions.POVariableExpression; import com.fujitsu.vdmj.tc.lex.TCNameSet; import com.fujitsu.vdmj.tc.lex.TCNameToken; +import com.fujitsu.vdmj.tc.types.TCOperationType; import com.fujitsu.vdmj.typechecker.NameScope; /** @@ -54,6 +56,23 @@ public TCNameSet caseVariableExpression(POVariableExpression node, Boolean updat return all; } + @Override + public TCNameSet caseApplyExpression(POApplyExpression node, Boolean updates) + { + TCNameSet all = super.caseApplyExpression(node, updates); + + if (node.type instanceof TCOperationType) + { + if (node.root instanceof POVariableExpression) + { + POVariableExpression name = (POVariableExpression)node.root; + all.add(name.name); + } + } + + return all; + } + @Override protected TCNameSet newCollection() { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/modules/POModule.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/modules/POModule.java index 3c17cc213..cc7e83b6a 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/modules/POModule.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/modules/POModule.java @@ -31,6 +31,8 @@ import com.fujitsu.vdmj.po.definitions.PODefinition; import com.fujitsu.vdmj.po.definitions.PODefinitionList; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; +import com.fujitsu.vdmj.pog.PONameContext; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.lex.TCIdentifierToken; import com.fujitsu.vdmj.tc.modules.TCModule; @@ -88,7 +90,14 @@ public ProofObligationList getProofObligations(MultiModuleEnvironment menv) ProofObligationList list = (annotations != null) ? annotations.poBefore(this) : new ProofObligationList(); - list.addAll(defs.getProofObligations(new POContextStack(), menv)); + for (PODefinition def: defs) + { + POContextStack ctxt = new POContextStack(); + ctxt.push(new PONameContext(def.getVariableNames())); + list.addAll(def.getProofObligations(ctxt, new POGState(), menv)); + ctxt.pop(); + } + list.typeCheck(tcmodule, menv); if (annotations != null) annotations.poAfter(this, list); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POBind.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POBind.java index 68cab131b..cc3f8ad1b 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POBind.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POBind.java @@ -31,6 +31,7 @@ import com.fujitsu.vdmj.po.PONode; import com.fujitsu.vdmj.po.patterns.visitors.POBindVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -57,7 +58,7 @@ public POBind(LexLocation location, POPattern pattern) abstract public List getMultipleBindList(); /** Return a list of POs. */ - abstract public ProofObligationList getProofObligations(POContextStack ctxt, Environment env); + abstract public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env); /** * Implemented by all binds to allow visitor processing. diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleBind.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleBind.java index abce9b694..d8c23cd72 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleBind.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleBind.java @@ -31,6 +31,7 @@ import com.fujitsu.vdmj.po.PONode; import com.fujitsu.vdmj.po.patterns.visitors.POMultipleBindVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -66,7 +67,7 @@ public List getMultipleBindList() } /** Get a list of POs. */ - abstract public ProofObligationList getProofObligations(POContextStack ctxt, Environment env); + abstract public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env); /** * Implemented by all multiple binds to allow visitor processing. diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleSeqBind.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleSeqBind.java index eded4aa79..c4709a94c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleSeqBind.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleSeqBind.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.po.patterns.visitors.POMultipleBindVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -48,9 +49,9 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return sequence.getProofObligations(ctxt, env); + return sequence.getProofObligations(ctxt, pogState, env); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleSetBind.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleSetBind.java index 92ad6832e..558a99a4b 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleSetBind.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleSetBind.java @@ -27,6 +27,7 @@ import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.po.patterns.visitors.POMultipleBindVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -48,9 +49,9 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return set.getProofObligations(ctxt, env); + return set.getProofObligations(ctxt, pogState, env); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleTypeBind.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleTypeBind.java index 845cb9f90..11abba6f1 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleTypeBind.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POMultipleTypeBind.java @@ -26,6 +26,7 @@ import com.fujitsu.vdmj.po.patterns.visitors.POMultipleBindVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.typechecker.Environment; @@ -48,7 +49,7 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { return new ProofObligationList(); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POSeqBind.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POSeqBind.java index e1c3bad48..ea82c081f 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POSeqBind.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POSeqBind.java @@ -30,6 +30,7 @@ import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.po.patterns.visitors.POBindVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -61,9 +62,9 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return sequence.getProofObligations(ctxt, env); + return sequence.getProofObligations(ctxt, pogState, env); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POSetBind.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POSetBind.java index f277ae733..d777966ee 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POSetBind.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POSetBind.java @@ -30,6 +30,7 @@ import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.po.patterns.visitors.POBindVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.typechecker.Environment; @@ -61,9 +62,9 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return set.getProofObligations(ctxt, env); + return set.getProofObligations(ctxt, pogState, env); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POTypeBind.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POTypeBind.java index 57d0d2482..c6085baec 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POTypeBind.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/POTypeBind.java @@ -29,6 +29,7 @@ import com.fujitsu.vdmj.po.patterns.visitors.POBindVisitor; import com.fujitsu.vdmj.pog.POContextStack; +import com.fujitsu.vdmj.pog.POGState; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.typechecker.Environment; @@ -61,7 +62,7 @@ public String toString() } @Override - public ProofObligationList getProofObligations(POContextStack ctxt, Environment env) + public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { return new ProofObligationList(); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAssignmentStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAssignmentStatement.java index a9d7e201d..6dac5e905 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAssignmentStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAssignmentStatement.java @@ -86,7 +86,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog } obligations.addAll(target.getProofObligations(ctxt)); - obligations.addAll(exp.getProofObligations(ctxt, env)); + obligations.addAll(exp.getProofObligations(ctxt, pogState, env)); obligations.stateUpdate(pogState, exp); TCNameSet updates = this.apply(new POStatementStateFinder(), true); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallObjectStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallObjectStatement.java index 44ef22bb0..248cd6787 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallObjectStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallObjectStatement.java @@ -72,7 +72,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog for (POExpression exp: args) { - obligations.addAll(exp.getProofObligations(ctxt, env)); + obligations.addAll(exp.getProofObligations(ctxt, pogState, env)); } // We have to assume the operation call accesses state diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallStatement.java index a4be51307..91bf391e2 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallStatement.java @@ -60,7 +60,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog for (POExpression exp: args) { - obligations.addAll(exp.getProofObligations(ctxt, env)); + obligations.addAll(exp.getProofObligations(ctxt, pogState, env)); } // We have to assume the operation call accesses state diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POExitStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POExitStatement.java index 1d1b8a905..a50318293 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POExitStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POExitStatement.java @@ -56,7 +56,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog if (expression != null) { - obligations.addAll(expression.getProofObligations(ctxt, env)); + obligations.addAll(expression.getProofObligations(ctxt, pogState, env)); obligations.stateUpdate(pogState, expression); } 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 83feb5d96..9fe2023a4 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 @@ -59,7 +59,7 @@ public String toString() @Override public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList obligations = set.getProofObligations(ctxt, env); + ProofObligationList obligations = set.getProofObligations(ctxt, pogState, env); obligations.stateUpdate(pogState, set); ProofObligationList loops = statement.getProofObligations(ctxt, pogState, env); 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 6c0f40b78..39a81535c 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 @@ -65,13 +65,13 @@ public String toString() @Override public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList obligations = from.getProofObligations(ctxt, env); - obligations.addAll(to.getProofObligations(ctxt, env)); + ProofObligationList obligations = from.getProofObligations(ctxt, pogState, env); + obligations.addAll(to.getProofObligations(ctxt, pogState, env)); obligations.stateUpdate(pogState, from); if (by != null) { - obligations.addAll(by.getProofObligations(ctxt, env)); + obligations.addAll(by.getProofObligations(ctxt, pogState, env)); obligations.stateUpdate(pogState, by); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForPatternBindStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForPatternBindStatement.java index 9dd1f4393..736dd5cf8 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForPatternBindStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POForPatternBindStatement.java @@ -68,7 +68,7 @@ public String toString() @Override public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - ProofObligationList list = exp.getProofObligations(ctxt, env); + ProofObligationList list = exp.getProofObligations(ctxt, pogState, env); list.stateUpdate(pogState, exp); if (patternBind.pattern != null) @@ -82,7 +82,7 @@ else if (patternBind.bind instanceof POTypeBind) else if (patternBind.bind instanceof POSetBind) { POSetBind bind = (POSetBind)patternBind.bind; - list.addAll(bind.set.getProofObligations(ctxt, env)); + list.addAll(bind.set.getProofObligations(ctxt, pogState, env)); ctxt.push(new POForAllSequenceContext(bind, exp)); list.add(new SetMemberObligation(bind.pattern.getMatchingExpression(), bind.set, ctxt)); @@ -91,7 +91,7 @@ else if (patternBind.bind instanceof POSetBind) else if (patternBind.bind instanceof POSeqBind) { POSeqBind bind = (POSeqBind)patternBind.bind; - list.addAll(bind.sequence.getProofObligations(ctxt, env)); + list.addAll(bind.sequence.getProofObligations(ctxt, pogState, env)); ctxt.push(new POForAllSequenceContext(bind, exp)); list.add(new SeqMemberObligation(bind.pattern.getMatchingExpression(), bind.sequence, ctxt)); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POIfStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POIfStatement.java index 76eff7f92..f7d14e86a 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POIfStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POIfStatement.java @@ -78,7 +78,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog { POGStateList stateList = new POGStateList(); - ProofObligationList obligations = ifExp.getProofObligations(ctxt, env); + ProofObligationList obligations = ifExp.getProofObligations(ctxt, pogState, env); obligations.stateUpdate(pogState, ifExp); ctxt.push(new POImpliesContext(ifExp)); @@ -89,7 +89,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog for (POElseIfStatement stmt: elseList) { - ProofObligationList oblist = stmt.elseIfExp.getProofObligations(ctxt, env); + ProofObligationList oblist = stmt.elseIfExp.getProofObligations(ctxt, pogState, env); oblist.stateUpdate(pogState, stmt.elseIfExp); oblist.addAll(stmt.thenStmt.getProofObligations(ctxt, stateList.addCopy(pogState), env)); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POLetBeStStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POLetBeStStatement.java index a15aa0343..03c49c712 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POLetBeStStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POLetBeStStatement.java @@ -64,12 +64,12 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog { ProofObligationList obligations = new ProofObligationList(); obligations.add(new LetBeExistsObligation(this, ctxt)); - obligations.addAll(bind.getProofObligations(ctxt, env)); + obligations.addAll(bind.getProofObligations(ctxt, pogState, env)); if (suchThat != null) { ctxt.push(new POForAllContext(this)); - ProofObligationList oblist = suchThat.getProofObligations(ctxt, env); + ProofObligationList oblist = suchThat.getProofObligations(ctxt, pogState, env); oblist.stateUpdate(pogState, suchThat); obligations.addAll(oblist); ctxt.pop(); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POReturnStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POReturnStatement.java index 2a99e69bb..e15ecdeca 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POReturnStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POReturnStatement.java @@ -56,7 +56,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog if (expression != null) { - obligations.addAll(expression.getProofObligations(ctxt, env)); + obligations.addAll(expression.getProofObligations(ctxt, pogState, env)); obligations.stateUpdate(pogState, expression); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POSpecificationStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POSpecificationStatement.java index bfd8344e3..811ec2065 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POSpecificationStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POSpecificationStatement.java @@ -71,19 +71,19 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog { for (POErrorCase err: errors) { - obligations.addAll(err.left.getProofObligations(ctxt, env)); - obligations.addAll(err.right.getProofObligations(ctxt, env)); + obligations.addAll(err.left.getProofObligations(ctxt, pogState, env)); + obligations.addAll(err.right.getProofObligations(ctxt, pogState, env)); } } if (precondition != null) { - obligations.addAll(precondition.getProofObligations(ctxt, env)); + obligations.addAll(precondition.getProofObligations(ctxt, pogState, env)); } if (postcondition != null) { - obligations.addAll(postcondition.getProofObligations(ctxt, env)); + obligations.addAll(postcondition.getProofObligations(ctxt, pogState, env)); } return obligations; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POStartStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POStartStatement.java index 72dfbe97d..41d49ebf6 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POStartStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POStartStatement.java @@ -46,7 +46,7 @@ public POStartStatement(LexLocation location, POExpression obj) @Override public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return objects.getProofObligations(ctxt, env); + return objects.getProofObligations(ctxt, pogState, env); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POStopStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POStopStatement.java index bd51eb82a..166529741 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POStopStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POStopStatement.java @@ -46,7 +46,7 @@ public POStopStatement(LexLocation location, POExpression obj) @Override public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env) { - return objects.getProofObligations(ctxt, env); + return objects.getProofObligations(ctxt, pogState, env); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POTixeStmtAlternative.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POTixeStmtAlternative.java index 1298ae708..5d8452ff2 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POTixeStmtAlternative.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POTixeStmtAlternative.java @@ -68,14 +68,14 @@ else if (patternBind.bind instanceof POTypeBind) else if (patternBind.bind instanceof POSetBind) { POSetBind bind = (POSetBind)patternBind.bind; - list.addAll(bind.set.getProofObligations(ctxt, env)); + list.addAll(bind.set.getProofObligations(ctxt, pogState, env)); list.add(new SetMemberObligation(bind.pattern.getMatchingExpression(), bind.set, ctxt)); } else if (patternBind.bind instanceof POSeqBind) { POSeqBind bind = (POSeqBind)patternBind.bind; - list.addAll(bind.sequence.getProofObligations(ctxt, env)); + list.addAll(bind.sequence.getProofObligations(ctxt, pogState, env)); list.add(new SeqMemberObligation(bind.pattern.getMatchingExpression(), bind.sequence, ctxt)); } 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 503da5e7f..83595e303 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 @@ -75,14 +75,14 @@ else if (patternBind.bind instanceof POTypeBind) else if (patternBind.bind instanceof POSetBind) { POSetBind bind = (POSetBind)patternBind.bind; - list.addAll(bind.set.getProofObligations(ctxt, env)); + list.addAll(bind.set.getProofObligations(ctxt, pogState, env)); list.add(new SetMemberObligation(bind.pattern.getMatchingExpression(), bind.set, ctxt)); } else if (patternBind.bind instanceof POSeqBind) { POSeqBind bind = (POSeqBind)patternBind.bind; - list.addAll(bind.sequence.getProofObligations(ctxt, env)); + list.addAll(bind.sequence.getProofObligations(ctxt, pogState, env)); list.add(new SeqMemberObligation(bind.pattern.getMatchingExpression(), bind.sequence, ctxt)); } 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 acd4f568b..a0cbabb42 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 @@ -59,7 +59,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog ProofObligationList obligations = new ProofObligationList(); obligations.add(new WhileLoopObligation(this, ctxt)); - obligations.addAll(exp.getProofObligations(ctxt, env)); + obligations.addAll(exp.getProofObligations(ctxt, pogState, env)); obligations.stateUpdate(pogState, exp); ProofObligationList loops = statement.getProofObligations(ctxt, pogState, env); 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 c8336ab58..0365de1d7 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligationList.java @@ -256,7 +256,7 @@ private void typeCheck(ProofObligation obligation, String mname, Environment env POExpression poexp = ClassMapper.getInstance(PONode.MAPPINGS).convertLocal(tcexp); POContextStack stack = new POContextStack(); stack.push(new PONameContext()); // Must have one context - ProofObligationList popos = poexp.getProofObligations(stack, env); + ProofObligationList popos = poexp.getProofObligations(stack, new POGState(), env); obligation.setHasObligations(!popos.isEmpty()); } @@ -276,13 +276,14 @@ public ProofObligationList markUnchecked(String message) /** * Update the obligations in this list because of the current POGState and the state read - * by the expression. + * by the expression. This is used by various statements and definitions, to suppress + * obligations that cannot yet be checked. */ public void stateUpdate(POGState pstate, POExpression expression) { boolean readsState = expression.readsState(); - if (pstate.hasUpdatedState() && readsState) + if (readsState && pstate.hasUpdatedState()) { markUnchecked(ProofObligation.HAS_UPDATED_STATE); } From 7d48d6b9d4fdb75c1330b64234f2f66d513810d3 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Wed, 23 Oct 2024 12:21:16 +0100 Subject: [PATCH 7/9] Correction to StateInvariantObligation --- .../java/com/fujitsu/vdmj/pog/StateInvariantObligation.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 3ad626911..f8d2d1d65 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInvariantObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInvariantObligation.java @@ -54,7 +54,7 @@ public StateInvariantObligation(POAssignmentStatement ass, POContextStack ctxt) sb.append("let "); sb.append(def.invPattern); sb.append(" = "); - sb.append(def.name); + sb.append(def.toPattern()); sb.append(" in "); sb.append(def.invExpression); } From d0c2b129a816ebab48e919b020a546ece9080920 Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Wed, 23 Oct 2024 12:49:32 +0100 Subject: [PATCH 8/9] Added toPattern in state designator --- .../vdmj/po/statements/POIdentifierDesignator.java | 6 ++++++ .../vdmj/po/statements/POStateDesignator.java | 9 +++++++++ .../java/com/fujitsu/vdmj/pog/ProofObligation.java | 1 + .../fujitsu/vdmj/pog/StateInvariantObligation.java | 13 ++++++++++--- 4 files changed, 26 insertions(+), 3 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POIdentifierDesignator.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POIdentifierDesignator.java index a84c55f8a..dd6953227 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POIdentifierDesignator.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POIdentifierDesignator.java @@ -42,4 +42,10 @@ public String toString() { return name.getName(); } + + @Override + public String toPattern() throws IllegalArgumentException + { + return name.getName(); + } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POStateDesignator.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POStateDesignator.java index c269f69c9..0d83d3719 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POStateDesignator.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POStateDesignator.java @@ -45,6 +45,15 @@ public POStateDesignator(LexLocation location) @Override abstract public String toString(); + + /** + * A pattern, such that "let = in ..." can be used in POs. This + * is not always possible. + */ + public String toPattern() throws IllegalArgumentException + { + throw new IllegalArgumentException("Cannot generate pattern for " + this); + } /** * @param ctxt 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 c5fc1f900..b80855701 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java @@ -60,6 +60,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 modifies state"; public static final String HAS_UPDATED_STATE = "Previous statements updated state"; + public static final String COMPLEX_ASSIGNMENT = "Assignment too complex"; public final LexLocation location; public final POType kind; 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 f8d2d1d65..558dd349c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInvariantObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInvariantObligation.java @@ -40,8 +40,15 @@ public StateInvariantObligation(POAssignmentStatement ass, POContextStack ctxt) super(ass.location, POType.STATE_INVARIANT, ctxt); StringBuilder sb = new StringBuilder(); - // Note a StateDesignator is not a pattern, so this may not work! - sb.append("let " + ass.target + " = " + ass.exp + " in\n"); + try + { + sb.append("let " + ass.target.toPattern() + " = " + ass.exp + " in\n"); + } + catch (IllegalArgumentException e) + { + // Can't represent designator as a pattern, so cannot check PO + markUnchecked(ProofObligation.COMPLEX_ASSIGNMENT); + } if (ass.classDefinition != null) { @@ -55,7 +62,7 @@ public StateInvariantObligation(POAssignmentStatement ass, POContextStack ctxt) sb.append(def.invPattern); sb.append(" = "); sb.append(def.toPattern()); - sb.append(" in "); + sb.append(" in\n"); sb.append(def.invExpression); } From 1fa92f3901593acae0d591aeb5d97a3bb6abdf0b Mon Sep 17 00:00:00 2001 From: Nick Battle Date: Thu, 24 Oct 2024 09:06:47 +0100 Subject: [PATCH 9/9] Tidy ApplyExpression and ignore return state changes --- .../po/expressions/POApplyExpression.java | 98 ++++++++++--------- .../vdmj/po/statements/POReturnStatement.java | 5 +- 2 files changed, 53 insertions(+), 50 deletions(-) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java index a6d372e1c..e51c34529 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java @@ -89,70 +89,72 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog { ProofObligationList obligations = new ProofObligationList(); - if (!type.isUnknown(location) && type.isMap(location)) + if (!type.isUnknown(location)) { - TCMapType m = type.getMap(); - obligations.add(new MapApplyObligation(root, args.get(0), ctxt)); - TCType atype = ctxt.checkType(args.get(0), argtypes.get(0)); - - if (!TypeComparator.isSubType(atype, m.from)) + if (type.isOperation(location)) { - obligations.add(new SubTypeObligation(args.get(0), m.from, atype, ctxt)); + pogState.didUpdateState(); // Operation calls assumed to update state } - } - - if (!type.isUnknown(location) && - (type.isFunction(location) || type.isOperation(location))) - { - String prename = root.getPreName(); - if (type.isFunction(location) && prename != null && !prename.isEmpty()) + if (type.isMap(location)) { - obligations.add(new FunctionApplyObligation(root, args, prename, ctxt)); + TCMapType m = type.getMap(); + obligations.add(new MapApplyObligation(root, args.get(0), ctxt)); + TCType atype = ctxt.checkType(args.get(0), argtypes.get(0)); + + if (!TypeComparator.isSubType(atype, m.from)) + { + obligations.add(new SubTypeObligation(args.get(0), m.from, atype, ctxt)); + } } - if (type.isOperation(location)) + if (type.isFunction(location) || type.isOperation(location)) { - pogState.didUpdateState(); // Operation calls assumed to update state - } - - TCTypeList paramTypes = type.isFunction(location) ? - type.getFunction().parameters : type.getOperation().parameters; + String prename = root.getPreName(); + + if (type.isFunction(location) && prename != null && !prename.isEmpty()) + { + obligations.add(new FunctionApplyObligation(root, args, prename, ctxt)); + } - int i=0; - - for (TCType at: argtypes) - { - at = ctxt.checkType(args.get(i), at); - TCType pt = paramTypes.get(i); - - if (!TypeComparator.isSubType(at, pt)) + TCTypeList paramTypes = type.isFunction(location) ? + type.getFunction().parameters : type.getOperation().parameters; + + int i=0; + + for (TCType at: argtypes) { - obligations.add(new SubTypeObligation(args.get(i), pt, at, ctxt)); + at = ctxt.checkType(args.get(i), at); + TCType pt = paramTypes.get(i); + + if (!TypeComparator.isSubType(at, pt)) + { + obligations.add(new SubTypeObligation(args.get(i), pt, at, ctxt)); + } + + i++; } - - i++; } - } - - if (!type.isUnknown(location) && type.isFunction(location)) - { - if (recursiveCycles != null) // name is a function in a recursive loop + + if (type.isFunction(location)) { - /** - * All of the functions in the loop will generate similar obligations, - * so the "add" method eliminates any duplicates. - */ - for (PODefinitionList loop: recursiveCycles) + if (recursiveCycles != null) // name is a function in a recursive loop { - obligations.add(new RecursiveObligation(location, loop, this, ctxt)); + /** + * All of the functions in the loop will generate similar obligations, + * so the "add" method eliminates any duplicates. + */ + for (PODefinitionList loop: recursiveCycles) + { + obligations.add(new RecursiveObligation(location, loop, this, ctxt)); + } } } - } - - if (!type.isUnknown(location) && type.isSeq(location)) - { - obligations.add(new SeqApplyObligation(root, args.get(0), ctxt)); + + if (type.isSeq(location)) + { + obligations.add(new SeqApplyObligation(root, args.get(0), ctxt)); + } } obligations.addAll(root.getProofObligations(ctxt, pogState, env)); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POReturnStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POReturnStatement.java index e15ecdeca..90510f5b2 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POReturnStatement.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POReturnStatement.java @@ -56,8 +56,9 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog if (expression != null) { - obligations.addAll(expression.getProofObligations(ctxt, pogState, env)); - obligations.stateUpdate(pogState, expression); + // Don't process POG state here, because we're returning, so the expression can + // have no further effect in the operation. + obligations.addAll(expression.getProofObligations(ctxt, new POGState(), env)); } return obligations;