diff --git a/annotations/src/main/java/annotations/ast/ASTConjectureAnnotation.java b/annotations/src/main/java/annotations/ast/ASTConjectureAnnotation.java index 7fc33193a..3a265dfa3 100644 --- a/annotations/src/main/java/annotations/ast/ASTConjectureAnnotation.java +++ b/annotations/src/main/java/annotations/ast/ASTConjectureAnnotation.java @@ -43,9 +43,9 @@ public ASTConjectureAnnotation(LexIdentifierToken name) } @Override - public ASTExpressionList parse(LexTokenReader ltr) throws LexException, ParserException + public void parse(LexTokenReader ltr) throws LexException, ParserException { - ASTExpressionList args = new ASTExpressionList(); + this.args = new ASTExpressionList(); try { @@ -75,8 +75,5 @@ public ASTExpressionList parse(LexTokenReader ltr) throws LexException, ParserEx // cause this annotation to be ignored. args.clear(); } - - return args; } - } diff --git a/annotations2/src/main/java/annotations/ast/ASTGhostAnnotation.java b/annotations2/src/main/java/annotations/ast/ASTGhostAnnotation.java index ec3ba1430..56b1f09b6 100644 --- a/annotations2/src/main/java/annotations/ast/ASTGhostAnnotation.java +++ b/annotations2/src/main/java/annotations/ast/ASTGhostAnnotation.java @@ -52,10 +52,11 @@ public ASTGhostAnnotation(LexIdentifierToken name) * Override the default parse, and look for @Ghost = ; */ @Override - public ASTExpressionList parse(LexTokenReader ltr) throws LexException, ParserException + public void parse(LexTokenReader ltr) throws LexException, ParserException { + this.args = new ASTExpressionList(); + ltr.nextToken(); - ASTExpressionList args = new ASTExpressionList(); ExpressionReader er = new ExpressionReader(ltr); ASTExpression exp = er.readExpression(); @@ -82,7 +83,5 @@ public ASTExpressionList parse(LexTokenReader ltr) throws LexException, ParserEx { parseException("missing ;", ltr.getLast().location); } - - return args; } } diff --git a/examples/quickcheck/TODO b/examples/quickcheck/TODO index e07f8da70..f1245d927 100644 --- a/examples/quickcheck/TODO +++ b/examples/quickcheck/TODO @@ -3,5 +3,4 @@ Things still to do with QuickCheck 1. Make getValues interruptible as well as checkObligations? 2. Move QC to be part of POPlugin(s) 3. Separate IO from calculations (and allow LSP control) -4. Make SearchQCPlugin use the "sense" of forall/exists to choose values. -6. Add -file and -func PO selection options? \ No newline at end of file +4. Add -file and -func PO selection options? \ No newline at end of file diff --git a/examples/quickcheck/src/main/java/annotations/IterableContext.java b/examples/quickcheck/src/main/java/annotations/IterableContext.java new file mode 100644 index 000000000..d815b11c2 --- /dev/null +++ b/examples/quickcheck/src/main/java/annotations/IterableContext.java @@ -0,0 +1,90 @@ +/******************************************************************************* + * + * Copyright (c) 2023 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 annotations; + +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.Vector; + +import com.fujitsu.vdmj.lex.LexLocation; +import com.fujitsu.vdmj.runtime.Context; +import com.fujitsu.vdmj.tc.lex.TCNameToken; +import com.fujitsu.vdmj.values.Value; + +/** + * A Context that is backed by a list of maps, which can be iterated through. + * This is used in QuickCheck to load a context with one of a selection of + * ParameterType settings. + */ +public class IterableContext extends Context +{ + private static final long serialVersionUID = 1L; + private final List> maps; + private int nextMap = 0; + + public IterableContext(LexLocation location, String title, Context outer) + { + super(location, title, outer); + maps = new Vector>(); + } + + public Map newMap(int index) + { + if (index < maps.size()) + { + return maps.get(index); + } + else + { + Map values = new HashMap(); + maps.add(values); + return values; + } + } + + public boolean hasNext() + { + return nextMap < maps.size(); + } + + public void next() + { + this.clear(); + this.putAll(maps.get(nextMap)); + nextMap++; + } + + public void setDefaults(TCNameToken name, Value value) + { + for (Map map: maps) + { + if (!map.containsKey(name)) + { + map.put(name, value); + } + } + } +} diff --git a/examples/quickcheck/src/main/java/annotations/ast/ASTQuickCheckAnnotation.java b/examples/quickcheck/src/main/java/annotations/ast/ASTQuickCheckAnnotation.java new file mode 100644 index 000000000..8c97cb7b5 --- /dev/null +++ b/examples/quickcheck/src/main/java/annotations/ast/ASTQuickCheckAnnotation.java @@ -0,0 +1,95 @@ +/******************************************************************************* + * + * Copyright (c) 2023 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 annotations.ast; + +import com.fujitsu.vdmj.ast.annotations.ASTAnnotation; +import com.fujitsu.vdmj.ast.lex.LexIdentifierToken; +import com.fujitsu.vdmj.ast.types.ASTParameterType; +import com.fujitsu.vdmj.ast.types.ASTType; +import com.fujitsu.vdmj.ast.types.ASTTypeList; +import com.fujitsu.vdmj.lex.LexException; +import com.fujitsu.vdmj.lex.LexTokenReader; +import com.fujitsu.vdmj.lex.Token; +import com.fujitsu.vdmj.syntax.ParserException; +import com.fujitsu.vdmj.syntax.TypeReader; +import com.fujitsu.vdmj.util.Utils; + +public class ASTQuickCheckAnnotation extends ASTAnnotation +{ + private static final long serialVersionUID = 1L; + + public ASTParameterType qcParam = null; + public ASTTypeList qcTypes = null; + + public ASTQuickCheckAnnotation(LexIdentifierToken name) + { + super(name); + } + + @Override + public String toString() + { + return "@" + name + " " + qcParam + " = " + Utils.listToString("", qcTypes, ", ", ";"); + } + + /** + * Override the default parse, and look for @QuickCheck @T = [,*]; + */ + @Override + public void parse(LexTokenReader ltr) throws LexException, ParserException + { + ltr.nextToken(); + TypeReader er = new TypeReader(ltr); + ASTType start = er.readType(); + + if (start instanceof ASTParameterType) + { + qcParam = (ASTParameterType)start; + qcTypes = new ASTTypeList(); + + if (!ltr.getLast().is(Token.EQUALS)) + { + parseException("expecting @T = ;", qcParam.location); + } + + do + { + ltr.nextToken(); + ASTType type = er.readType(); + qcTypes.add(type); + } + while (ltr.getLast().is(Token.COMMA)); + } + else + { + parseException("expecting @T = [,*];", start.location); + } + + if (ltr.getLast().isNot(Token.SEMICOLON)) + { + parseException("missing ;", ltr.getLast().location); + } + } +} diff --git a/examples/quickcheck/src/main/java/annotations/po/POQuickCheckAnnotation.java b/examples/quickcheck/src/main/java/annotations/po/POQuickCheckAnnotation.java new file mode 100644 index 000000000..001f4f850 --- /dev/null +++ b/examples/quickcheck/src/main/java/annotations/po/POQuickCheckAnnotation.java @@ -0,0 +1,52 @@ +/******************************************************************************* + * + * Copyright (c) 2018 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 annotations.po; + +import com.fujitsu.vdmj.po.annotations.POAnnotation; +import com.fujitsu.vdmj.tc.lex.TCIdentifierToken; +import com.fujitsu.vdmj.tc.types.TCParameterType; +import com.fujitsu.vdmj.tc.types.TCTypeList; +import com.fujitsu.vdmj.util.Utils; + +public class POQuickCheckAnnotation extends POAnnotation +{ + private static final long serialVersionUID = 1L; + + public final TCParameterType qcParam; + public final TCTypeList qcTypes; + + public POQuickCheckAnnotation(TCIdentifierToken name, TCParameterType qcParam, TCTypeList qcTypes) + { + super(name, null); + this.qcParam = qcParam; + this.qcTypes = qcTypes; + } + + @Override + public String toString() + { + return "@" + name + " " + qcParam + " = " + Utils.listToString("", qcTypes, ", ", ";"); + } +} diff --git a/examples/quickcheck/src/main/java/annotations/tc/TCQuickCheckAnnotation.java b/examples/quickcheck/src/main/java/annotations/tc/TCQuickCheckAnnotation.java new file mode 100644 index 000000000..e4fa5e7c9 --- /dev/null +++ b/examples/quickcheck/src/main/java/annotations/tc/TCQuickCheckAnnotation.java @@ -0,0 +1,125 @@ +/******************************************************************************* + * + * Copyright (c) 2018 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 annotations.tc; + +import com.fujitsu.vdmj.tc.annotations.TCAnnotation; +import com.fujitsu.vdmj.tc.definitions.TCClassDefinition; +import com.fujitsu.vdmj.tc.definitions.TCDefinition; +import com.fujitsu.vdmj.tc.definitions.TCExplicitFunctionDefinition; +import com.fujitsu.vdmj.tc.definitions.TCImplicitFunctionDefinition; +import com.fujitsu.vdmj.tc.expressions.TCExpression; +import com.fujitsu.vdmj.tc.lex.TCIdentifierToken; +import com.fujitsu.vdmj.tc.modules.TCModule; +import com.fujitsu.vdmj.tc.statements.TCStatement; +import com.fujitsu.vdmj.tc.types.TCParameterType; +import com.fujitsu.vdmj.tc.types.TCType; +import com.fujitsu.vdmj.tc.types.TCTypeList; +import com.fujitsu.vdmj.typechecker.Environment; +import com.fujitsu.vdmj.typechecker.NameScope; +import com.fujitsu.vdmj.util.Utils; + +public class TCQuickCheckAnnotation extends TCAnnotation +{ + private static final long serialVersionUID = 1L; + + public final TCParameterType qcParam; + public final TCTypeList qcTypes; + + public TCQuickCheckAnnotation(TCIdentifierToken name, TCParameterType qcParam, TCTypeList qcTypes) + { + super(name, null); + this.qcParam = qcParam; + this.qcTypes = qcTypes; + } + + @Override + public String toString() + { + return "@" + name + " " + qcParam + " = " + Utils.listToString("", qcTypes, ", ", ";"); + } + + @Override + public void tcBefore(TCDefinition def, Environment env, NameScope scope) + { + TCTypeList funcParams = null; + + if (def instanceof TCExplicitFunctionDefinition) + { + TCExplicitFunctionDefinition exdef = (TCExplicitFunctionDefinition)def; + funcParams = exdef.typeParams; + } + else if (def instanceof TCImplicitFunctionDefinition) + { + TCImplicitFunctionDefinition imdef = (TCImplicitFunctionDefinition)def; + funcParams = imdef.typeParams; + } + else + { + name.report(6001, "@QuickCheck only applies to function definitions"); + return; + } + + if (funcParams == null) + { + name.report(6001, "@QuickCheck only applies to polymorphic definitions"); + } + else + { + for (TCType ptype: funcParams) + { + if (ptype.equals(qcParam)) + { + return; // Valid parameter name + } + } + + name.report(6001, "@QuickCheck " + qcParam + " is not a parameter of " + def.name); + } + } + + @Override + public void tcBefore(TCStatement stmt, Environment env, NameScope scope) + { + name.report(6001, "@QuickCheck only applies to function definitions"); + } + + @Override + public void tcBefore(TCExpression exp, Environment env, NameScope scope) + { + name.report(6001, "@QuickCheck only applies to function definitions"); + } + + @Override + public void tcBefore(TCModule m) + { + name.report(6001, "@QuickCheck only applies to function definitions"); + } + + @Override + public void tcBefore(TCClassDefinition m) + { + name.report(6001, "@QuickCheck only applies to function definitions"); + } +} diff --git a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java index d113c69c1..212ce52be 100644 --- a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -42,6 +42,7 @@ import com.fujitsu.vdmj.in.expressions.INExpression; import com.fujitsu.vdmj.in.patterns.INBindingSetter; import com.fujitsu.vdmj.mapper.ClassMapper; +import com.fujitsu.vdmj.po.annotations.POAnnotation; import com.fujitsu.vdmj.pog.POStatus; import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; @@ -52,11 +53,17 @@ import com.fujitsu.vdmj.tc.expressions.TCExistsExpression; import com.fujitsu.vdmj.tc.expressions.TCExpression; import com.fujitsu.vdmj.tc.lex.TCNameToken; +import com.fujitsu.vdmj.tc.types.TCParameterType; +import com.fujitsu.vdmj.tc.types.TCRealType; +import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.util.GetResource; import com.fujitsu.vdmj.values.BooleanValue; +import com.fujitsu.vdmj.values.ParameterValue; import com.fujitsu.vdmj.values.Value; import com.fujitsu.vdmj.values.ValueList; +import annotations.IterableContext; +import annotations.po.POQuickCheckAnnotation; import quickcheck.strategies.QCStrategy; import quickcheck.strategies.Results; import quickcheck.visitors.FixedRangeCreator; @@ -121,7 +128,7 @@ else if ((names.isEmpty() && instance.useByDefault()) || names.contains(instance if (argvSize != argv.size()) { // Constructor took some arguments - errorln("The " + instance.getName() + " strategy is not enabled. Add -p " + instance.getName()); + errorln("The " + instance.getName() + " strategy is not enabled. Add -s " + instance.getName()); errorCount++; } } @@ -208,7 +215,7 @@ public List strategyNames(List arglist) { String arg = iter.next(); - if (arg.equals("-p")) + if (arg.equals("-s")) { iter.remove(); @@ -220,7 +227,7 @@ public List strategyNames(List arglist) } else { - errorln("-p must be followed by a strategy name"); + errorln("-s must be followed by a strategy name"); names.add("unknown"); } } @@ -303,42 +310,47 @@ public Results getValues(ProofObligation po) if (!po.isCheckable) { - return new Results(proved, union, 0); + return new Results(false, union, 0); } INExpression exp = getINExpression(po); List binds = getINBindList(exp); long before = System.currentTimeMillis(); + IterableContext ictxt = addTypeParams(po, Interpreter.getInstance().getInitialContext()); - for (QCStrategy strategy: strategies) + while (ictxt.hasNext()) { - Results presults = strategy.getValues(po, exp, binds); - Map cexamples = presults.counterexamples; + ictxt.next(); - for (String bind: cexamples.keySet()) + for (QCStrategy strategy: strategies) { - if (union.containsKey(bind)) - { - union.get(bind).addAll(cexamples.get(bind)); - } - else + Results presults = strategy.getValues(po, exp, binds, ictxt); + Map cexamples = presults.counterexamples; + + for (String bind: cexamples.keySet()) { - union.put(bind, cexamples.get(bind)); + if (union.containsKey(bind)) + { + union.get(bind).addAll(cexamples.get(bind)); + } + else + { + union.put(bind, cexamples.get(bind)); + } } + + proved |= presults.proved; } - - proved |= presults.proved; - } - for (INBindingSetter bind: binds) - { - if (!union.containsKey(bind.toString())) + for (INBindingSetter bind: binds) { - // Generate some values for missing bindings, using the fixed method - RootContext ctxt = Interpreter.getInstance().getInitialContext(); - ValueList list = new ValueList(); - list.addAll(bind.getType().apply(new FixedRangeCreator(ctxt), 10)); - union.put(bind.toString(), list); + if (!union.containsKey(bind.toString())) + { + // Generate some values for missing bindings, using the fixed method + ValueList list = new ValueList(); + list.addAll(bind.getType().apply(new FixedRangeCreator(ictxt), 10)); + union.put(bind.toString(), list); + } } } @@ -368,7 +380,7 @@ else if (results.proved && results.counterexamples.isEmpty() && !bindings.isEmpty()) // empty binds => simple forall over sets, so must execute { - po.status = POStatus.PROVED; + po.setStatus(POStatus.PROVED); printf("PO #%d, PROVED %s\n", po.number, duration(results.duration)); return; } @@ -397,10 +409,18 @@ else if (results.proved && Value result = new BooleanValue(false); ContextException exception = null; + IterableContext ictxt = addTypeParams(po, ctxt); + try { verbose("PO #%d, starting...\n", po.number); - result = poexp.eval(ctxt); + + do + { + ictxt.next(); + result = poexp.eval(ictxt); + } + while (ictxt.hasNext() && result.boolValue(ctxt)); } catch (ContextException e) { @@ -428,28 +448,31 @@ else if (result instanceof BooleanValue) { if (result.boolValue(ctxt)) { - String outcome = null; + POStatus outcome = null; if (po.getCheckedExpression() instanceof TCExistsExpression) { - outcome = "PROVED"; // An "exists" PO is PROVED, if true. + outcome = POStatus.PROVED; // An "exists" PO is PROVED, if true. } else { - outcome = (results.proved) ? "PROVED" : "MAYBE"; + outcome = (results.proved) ? POStatus.PROVED : POStatus.MAYBE; } - printf("PO #%d, %s %s\n", po.number, outcome, duration(before, after)); + printf("PO #%d, %s %s\n", po.number, outcome.toString().toUpperCase(), duration(before, after)); + po.setStatus(outcome); } else { if (po.getCheckedExpression() instanceof TCExistsExpression) { printf("PO #%d, MAYBE %s\n", po.number, duration(before, after)); + po.setStatus(POStatus.MAYBE); } else { printf("PO #%d, FAILED %s: ", po.number, duration(before, after)); + po.setStatus(POStatus.FAILED); printFailPath(bindings); if (exception != null) @@ -465,6 +488,7 @@ else if (result instanceof BooleanValue) else { printf("PO #%d, Error: PO evaluation returns %s?\n", po.number, result.kind()); + po.setStatus(POStatus.FAILED); println("----"); printBindings(bindings); println("----"); @@ -474,6 +498,7 @@ else if (result instanceof BooleanValue) catch (Exception e) { printf("PO #%d, Exception: %s\n", po.number, e.getMessage()); + po.setStatus(POStatus.FAILED); println("----"); printBindings(bindings); println("----"); @@ -497,6 +522,49 @@ else if (result instanceof BooleanValue) } } + private IterableContext addTypeParams(ProofObligation po, Context ctxt) + { + IterableContext ictxt = new IterableContext(po.location, "Type params", ctxt); + + if (po.typeParams != null) + { + if (po.annotations != null) + { + for (POAnnotation a: po.annotations) + { + if (a instanceof POQuickCheckAnnotation) + { + POQuickCheckAnnotation qca = (POQuickCheckAnnotation)a; + int index = 0; + + for (TCType ptype: qca.qcTypes) + { + Map map = ictxt.newMap(index++); + map.put(qca.qcParam.name, new ParameterValue(ptype)); + } + } + } + } + + if (!ictxt.hasNext()) // Still empty after any annotations + { + ictxt.newMap(0); // So something to hold defaults + } + + for (TCType type: po.typeParams) + { + TCParameterType ptype = (TCParameterType)type; + ictxt.setDefaults(ptype.name, new ParameterValue(new TCRealType(po.location))); + } + } + else + { + ictxt.newMap(0); // So hasNext() and next() work + } + + return ictxt; + } + private void printBindings(List bindings) { int MAXVALUES = 10; diff --git a/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java b/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java index 35925edc3..8dcd8b058 100644 --- a/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java +++ b/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java @@ -44,7 +44,7 @@ public class QuickCheckCommand extends AnalysisCommand { - private final static String CMD = "quickcheck [-?|-help][-p ]* [-]* []"; + private final static String CMD = "quickcheck [-?|-help][-s ]* [-]* []"; private final static String USAGE = "Usage: " + CMD; public QuickCheckCommand(String line) @@ -90,7 +90,7 @@ public String run(String line) if (!qc.getDisabledStrategies().isEmpty()) { - println("Disabled strategies (add with -p ):"); + println("Disabled strategies (add with -s ):"); for (QCStrategy strategy: qc.getDisabledStrategies()) { diff --git a/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckExecutor.java b/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckExecutor.java index b0caf44c7..71e022982 100644 --- a/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckExecutor.java +++ b/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckExecutor.java @@ -34,8 +34,10 @@ import dap.DAPRequest; import dap.DAPResponse; import json.JSONObject; +import lsp.LSPServer; import quickcheck.QuickCheck; import quickcheck.strategies.Results; +import rpc.RPCRequest; import workspace.PluginRegistry; import workspace.plugins.POPlugin; @@ -102,8 +104,13 @@ protected void error(Throwable e) throws IOException } @Override - protected void clean() + protected void clean() throws IOException { + // Always kick the (LSP) client, since the PO statuses may have been updated... + LSPServer lsp = LSPServer.getInstance(); + lsp.writeMessage(RPCRequest.notification("slsp/POG/updated", + new JSONObject("successful", true))); + running = null; } } diff --git a/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckLSPCommand.java b/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckLSPCommand.java index fe5dc480b..4944ea60c 100644 --- a/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckLSPCommand.java +++ b/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckLSPCommand.java @@ -39,7 +39,7 @@ public class QuickCheckLSPCommand extends AnalysisCommand { - public final static String CMD = "quickcheck [-?|-help][-p ]* [-]* []"; + public final static String CMD = "quickcheck [-?|-help][-s ]* [-]* []"; private final static String USAGE = "Usage: " + CMD; public QuickCheckLSPCommand(String line) @@ -97,7 +97,7 @@ public DAPMessageList run(DAPRequest request) if (!qc.getDisabledStrategies().isEmpty()) { - println("Disabled strategies (add with -p ):"); + println("Disabled strategies (add with -s ):"); for (QCStrategy strategy: qc.getDisabledStrategies()) { @@ -145,4 +145,10 @@ public boolean notWhenRunning() { return true; } + + @Override + public boolean notWhenDirty() + { + return true; + } } diff --git a/examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java b/examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java index 495cd7d6c..e089e4ea0 100644 --- a/examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java +++ b/examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java @@ -38,7 +38,6 @@ import com.fujitsu.vdmj.messages.InternalException; import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.runtime.Context; -import com.fujitsu.vdmj.runtime.Interpreter; import com.fujitsu.vdmj.values.ValueList; import quickcheck.QuickCheck; @@ -122,7 +121,7 @@ public boolean init(QuickCheck qc) } @Override - public Results getValues(ProofObligation po, INExpression exp, List binds) + public Results getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) { HashMap result = new HashMap(); long before = System.currentTimeMillis(); @@ -130,7 +129,6 @@ public Results getValues(ProofObligation po, INExpression exp, List readRangeFile(String filename) + private Map readRangeFile(QuickCheck qc, String filename) { try { @@ -226,7 +236,8 @@ private Map readRangeFile(String filename) for (int i=0; i ranges = new HashMap(); long before = System.currentTimeMillis(); printf("Expanding " + inbinds.size() + " ranges: "); for (int i=0; i tparams = mtb.type.apply(new TCParameterCollector(), null); + + if (!tparams.isEmpty()) + { + TCDefinitionList defs = new TCDefinitionList(); + + for (TCParameterType tparam: tparams) + { + TCDefinition p = new TCLocalDefinition(mtb.type.location, tparam.name, tparam); + p.markUsed(); + defs.add(p); + } + + return new FlatEnvironment(defs, env); + } + } + + return env; + } + + private Context addTypeParams(TCMultipleBind bind, RootContext ctxt) + { + if (bind instanceof TCMultipleTypeBind) + { + TCMultipleTypeBind mbind = (TCMultipleTypeBind)bind; + List ptypes = mbind.type.apply(new TCParameterCollector(), null); + Context params = new Context(bind.location, "Type params", ctxt); + + for (TCParameterType ptype: ptypes) + { + // Just map all @T params to "real" as the ranges.qc value will decide + params.put(ptype.name, new ParameterValue(new TCRealType(ptype.location))); + } + + return params; + } + else + { + return ctxt; + } + } @Override public String getName() @@ -425,7 +506,7 @@ public boolean init(QuickCheck qc) if (new File(rangesFile).exists()) { println("Using ranges file " + rangesFile); - allRanges = readRangeFile(rangesFile); + allRanges = readRangeFile(qc, rangesFile); } else { @@ -438,7 +519,7 @@ public boolean init(QuickCheck qc) } @Override - public Results getValues(ProofObligation po, INExpression exp, List binds) + public Results getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) { Map values = new HashMap(); long before = System.currentTimeMillis(); @@ -473,6 +554,6 @@ public String help() @Override public boolean useByDefault() { - return false; // Use if no -p given + return false; // Use if no -s given } } diff --git a/examples/quickcheck/src/main/java/quickcheck/strategies/QCStrategy.java b/examples/quickcheck/src/main/java/quickcheck/strategies/QCStrategy.java index a38e420c6..a0ad97ba2 100644 --- a/examples/quickcheck/src/main/java/quickcheck/strategies/QCStrategy.java +++ b/examples/quickcheck/src/main/java/quickcheck/strategies/QCStrategy.java @@ -29,6 +29,7 @@ import com.fujitsu.vdmj.in.expressions.INExpression; import com.fujitsu.vdmj.in.patterns.INBindingSetter; import com.fujitsu.vdmj.pog.ProofObligation; +import com.fujitsu.vdmj.runtime.Context; import quickcheck.QuickCheck; @@ -38,6 +39,6 @@ abstract public class QCStrategy abstract public boolean hasErrors(); abstract public boolean useByDefault(); abstract public boolean init(QuickCheck qc); - abstract public Results getValues(ProofObligation po, INExpression exp, List binds); + abstract public Results getValues(ProofObligation po, INExpression exp, List binds, Context ctxt); abstract public String help(); } diff --git a/examples/quickcheck/src/main/java/quickcheck/strategies/RandomQCStrategy.java b/examples/quickcheck/src/main/java/quickcheck/strategies/RandomQCStrategy.java index 08c12caa2..249f642e0 100644 --- a/examples/quickcheck/src/main/java/quickcheck/strategies/RandomQCStrategy.java +++ b/examples/quickcheck/src/main/java/quickcheck/strategies/RandomQCStrategy.java @@ -34,8 +34,7 @@ import com.fujitsu.vdmj.in.expressions.INExpression; import com.fujitsu.vdmj.in.patterns.INBindingSetter; import com.fujitsu.vdmj.pog.ProofObligation; -import com.fujitsu.vdmj.runtime.Interpreter; -import com.fujitsu.vdmj.runtime.RootContext; +import com.fujitsu.vdmj.runtime.Context; import com.fujitsu.vdmj.values.ValueList; import com.fujitsu.vdmj.values.ValueSet; @@ -128,15 +127,13 @@ public boolean init(QuickCheck qc) } @Override - public Results getValues(ProofObligation po, INExpression exp, List binds) + public Results getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) { HashMap result = new HashMap(); long before = System.currentTimeMillis(); if (po.isCheckable && po.getCheckedExpression() != null) { - RootContext ctxt = Interpreter.getInstance().getInitialContext(); - for (INBindingSetter bind: binds) { RandomRangeCreator visitor = new RandomRangeCreator(ctxt, seed++); @@ -159,6 +156,6 @@ public String help() @Override public boolean useByDefault() { - return true; // Don't use if no -p given + return true; // Don't use if no -s given } } diff --git a/examples/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java b/examples/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java index c609730ee..24edea90b 100644 --- a/examples/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java +++ b/examples/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java @@ -32,8 +32,13 @@ import com.fujitsu.vdmj.in.expressions.INExpression; import com.fujitsu.vdmj.in.patterns.INBindingSetter; import com.fujitsu.vdmj.pog.ProofObligation; +import com.fujitsu.vdmj.runtime.Context; +import com.fujitsu.vdmj.runtime.ContextException; +import com.fujitsu.vdmj.runtime.ValueException; +import com.fujitsu.vdmj.tc.expressions.TCExistsExpression; import com.fujitsu.vdmj.values.NameValuePair; import com.fujitsu.vdmj.values.NameValuePairList; +import com.fujitsu.vdmj.values.Value; import com.fujitsu.vdmj.values.ValueList; import quickcheck.QuickCheck; @@ -78,14 +83,15 @@ public boolean init(QuickCheck qc) } @Override - public Results getValues(ProofObligation po, INExpression exp, List binds) + public Results getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) { HashMap result = new HashMap(); long before = System.currentTimeMillis(); if (po.isCheckable && po.getCheckedExpression() != null) { - NameValuePairList nvps = po.getCheckedExpression().apply(new SearchQCVisitor(), null); + boolean exists = po.getCheckedExpression() instanceof TCExistsExpression; + NameValuePairList nvps = po.getCheckedExpression().apply(new SearchQCVisitor(exists), null); for (NameValuePair pair: nvps) { @@ -96,15 +102,32 @@ public Results getValues(ProofObligation po, INExpression exp, List ...). So check. + + try { - ValueList current = result.get(key); - current.add(pair.value); + Value fixed = pair.value.convertTo(bind.getType(), ctxt); + + if (result.containsKey(key)) + { + ValueList current = result.get(key); + current.add(fixed); + } + else + { + result.put(key, new ValueList(fixed)); + } } - else + catch (ValueException e) { - result.put(key, new ValueList(pair.value)); + // ignore illegal values } + catch (ContextException e) + { + // ignore illegal values + } + break; } } @@ -123,6 +146,6 @@ public String help() @Override public boolean useByDefault() { - return true; // Use if no -p given + return true; // Use if no -s given } } diff --git a/examples/quickcheck/src/main/java/quickcheck/visitors/FixedRangeCreator.java b/examples/quickcheck/src/main/java/quickcheck/visitors/FixedRangeCreator.java index fa91c348b..58c56b6a4 100644 --- a/examples/quickcheck/src/main/java/quickcheck/visitors/FixedRangeCreator.java +++ b/examples/quickcheck/src/main/java/quickcheck/visitors/FixedRangeCreator.java @@ -49,6 +49,7 @@ import com.fujitsu.vdmj.tc.types.TCNaturalOneType; import com.fujitsu.vdmj.tc.types.TCNaturalType; import com.fujitsu.vdmj.tc.types.TCOptionalType; +import com.fujitsu.vdmj.tc.types.TCParameterType; import com.fujitsu.vdmj.tc.types.TCProductType; import com.fujitsu.vdmj.tc.types.TCQuoteType; import com.fujitsu.vdmj.tc.types.TCRationalType; @@ -80,6 +81,7 @@ import com.fujitsu.vdmj.values.NaturalValue; import com.fujitsu.vdmj.values.NilValue; import com.fujitsu.vdmj.values.ObjectValue; +import com.fujitsu.vdmj.values.ParameterValue; import com.fujitsu.vdmj.values.QuoteValue; import com.fujitsu.vdmj.values.RealValue; import com.fujitsu.vdmj.values.RecordValue; @@ -118,6 +120,13 @@ public ValueSet caseUnknownType(TCUnknownType node, Integer limit) // Anything... ? return caseBooleanType(new TCBooleanType(LexLocation.ANY), limit); } + + @Override + public ValueSet caseParameterType(TCParameterType node, Integer limit) + { + ParameterValue pv = (ParameterValue) ctxt.get(node.name); + return pv.type.apply(this, limit); + } @Override public ValueSet caseBooleanType(TCBooleanType type, Integer limit) diff --git a/examples/quickcheck/src/main/java/quickcheck/visitors/SearchQCVisitor.java b/examples/quickcheck/src/main/java/quickcheck/visitors/SearchQCVisitor.java index 891a48397..9753881d5 100644 --- a/examples/quickcheck/src/main/java/quickcheck/visitors/SearchQCVisitor.java +++ b/examples/quickcheck/src/main/java/quickcheck/visitors/SearchQCVisitor.java @@ -53,7 +53,7 @@ import com.fujitsu.vdmj.tc.types.TCNaturalType; import com.fujitsu.vdmj.tc.types.TCNumericType; import com.fujitsu.vdmj.tc.types.TCRealType; -import com.fujitsu.vdmj.tc.types.TCSeq1Type; +import com.fujitsu.vdmj.tc.types.TCSet1Type; import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.values.BooleanValue; import com.fujitsu.vdmj.values.IntegerValue; @@ -69,9 +69,12 @@ public class SearchQCVisitor extends TCLeafExpressionVisitor { - public SearchQCVisitor() + private final boolean exists; + + public SearchQCVisitor(boolean exists) { super(); + this.exists = exists; } @Override @@ -92,14 +95,30 @@ public NameValuePairList caseEqualsExpression(TCEqualsExpression node, Object ar if (node.right instanceof TCIntegerLiteralExpression) { TCIntegerLiteralExpression rhs = (TCIntegerLiteralExpression)node.right; - nvpl.add(var.name, new IntegerValue(rhs.value.value.add(BigInteger.ONE))); // ie. rhs + 1 is NOT = rhs + + if (exists) + { + nvpl.add(var.name, new IntegerValue(rhs.value.value)); + } + else + { + nvpl.add(var.name, new IntegerValue(rhs.value.value.add(BigInteger.ONE))); // ie. rhs + 1 is NOT = rhs + } } else if (node.right instanceof TCRealLiteralExpression) { try { TCRealLiteralExpression rhs = (TCRealLiteralExpression)node.right; - nvpl.add(var.name, new RealValue(rhs.value.value.add(BigDecimal.ONE))); // ie. rhs + 1 is NOT = rhs + + if (exists) + { + nvpl.add(var.name, new RealValue(rhs.value.value)); + } + else + { + nvpl.add(var.name, new RealValue(rhs.value.value.add(BigDecimal.ONE))); // ie. rhs + 1 is NOT = rhs + } } catch (Exception e) { @@ -110,7 +129,7 @@ else if (node.right instanceof TCSeqEnumExpression) { TCSeqEnumExpression rhs = (TCSeqEnumExpression)node.right; - if (!rhs.members.isEmpty()) // not empty sequence + if (!rhs.members.isEmpty() || exists) // not empty sequence, or empty and exists { nvpl.add(var.name, new SeqValue()); // ie. [] is NOT = rhs } @@ -119,7 +138,7 @@ else if (node.right instanceof TCSetEnumExpression) { TCSetEnumExpression rhs = (TCSetEnumExpression)node.right; - if (!rhs.members.isEmpty()) // not empty set + if (!rhs.members.isEmpty() || exists) // not empty set, or empty and exists { nvpl.add(var.name, new SetValue()); // ie. {} is NOT = rhs } @@ -141,14 +160,30 @@ public NameValuePairList caseNotEqualExpression(TCNotEqualExpression node, Objec if (node.right instanceof TCIntegerLiteralExpression) { TCIntegerLiteralExpression rhs = (TCIntegerLiteralExpression)node.right; - nvpl.add(var.name, new IntegerValue(rhs.value.value)); // ie. rhs is NOT <> rhs + + if (exists) + { + nvpl.add(var.name, new IntegerValue(rhs.value.value.add(BigInteger.ONE))); + } + else + { + nvpl.add(var.name, new IntegerValue(rhs.value.value)); // ie. rhs is NOT <> rhs + } } else if (node.right instanceof TCRealLiteralExpression) { try { TCRealLiteralExpression rhs = (TCRealLiteralExpression)node.right; - nvpl.add(var.name, new RealValue(rhs.value.value)); // ie. rhs is NOT <> rhs + + if (exists) + { + nvpl.add(var.name, new RealValue(rhs.value.value.add(BigDecimal.ONE))); + } + else + { + nvpl.add(var.name, new RealValue(rhs.value.value)); // ie. rhs is NOT <> rhs + } } catch (Exception e) { @@ -190,14 +225,30 @@ public NameValuePairList caseGreaterExpression(TCGreaterExpression node, Object if (node.right instanceof TCIntegerLiteralExpression) { TCIntegerLiteralExpression rhs = (TCIntegerLiteralExpression)node.right; - nvpl.add(var.name, new IntegerValue(rhs.value.value)); // ie. rhs is NOT > rhs + + if (exists) + { + nvpl.add(var.name, new IntegerValue(rhs.value.value.add(BigInteger.ONE))); + } + else + { + nvpl.add(var.name, new IntegerValue(rhs.value.value)); // ie. rhs is NOT > rhs + } } else if (node.right instanceof TCRealLiteralExpression) { try { TCRealLiteralExpression rhs = (TCRealLiteralExpression)node.right; - nvpl.add(var.name, new RealValue(rhs.value.value)); // ie. rhs is NOT > rhs + + if (exists) + { + nvpl.add(var.name, new RealValue(rhs.value.value.add(BigDecimal.ONE))); + } + else + { + nvpl.add(var.name, new RealValue(rhs.value.value)); // ie. rhs is NOT > rhs + } } catch (Exception e) { @@ -221,14 +272,30 @@ public NameValuePairList caseGreaterEqualExpression(TCGreaterEqualExpression nod if (node.right instanceof TCIntegerLiteralExpression) { TCIntegerLiteralExpression rhs = (TCIntegerLiteralExpression)node.right; - nvpl.add(var.name, new IntegerValue(rhs.value.value.subtract(BigInteger.ONE))); // ie. rhs-1 is NOT >= rhs + + if (exists) + { + nvpl.add(var.name, new IntegerValue(rhs.value.value)); + } + else + { + nvpl.add(var.name, new IntegerValue(rhs.value.value.subtract(BigInteger.ONE))); // ie. rhs-1 is NOT >= rhs + } } else if (node.right instanceof TCRealLiteralExpression) { try { TCRealLiteralExpression rhs = (TCRealLiteralExpression)node.right; - nvpl.add(var.name, new RealValue(rhs.value.value.subtract(BigDecimal.ONE))); // ie. rhs-1 is NOT >= rhs + + if (exists) + { + nvpl.add(var.name, new RealValue(rhs.value.value)); + } + else + { + nvpl.add(var.name, new RealValue(rhs.value.value.subtract(BigDecimal.ONE))); // ie. rhs-1 is NOT >= rhs + } } catch (Exception e) { @@ -252,14 +319,30 @@ public NameValuePairList caseLessExpression(TCLessExpression node, Object arg) if (node.right instanceof TCIntegerLiteralExpression) { TCIntegerLiteralExpression rhs = (TCIntegerLiteralExpression)node.right; - nvpl.add(var.name, new IntegerValue(rhs.value.value)); // ie. rhs is NOT < rhs + + if (exists) + { + nvpl.add(var.name, new IntegerValue(rhs.value.value.subtract(BigInteger.ONE))); + } + else + { + nvpl.add(var.name, new IntegerValue(rhs.value.value)); // ie. rhs is NOT < rhs + } } else if (node.right instanceof TCRealLiteralExpression) { try { TCRealLiteralExpression rhs = (TCRealLiteralExpression)node.right; - nvpl.add(var.name, new RealValue(rhs.value.value)); // ie. rhs is NOT < rhs + + if (exists) + { + nvpl.add(var.name, new RealValue(rhs.value.value.subtract(BigDecimal.ONE))); + } + else + { + nvpl.add(var.name, new RealValue(rhs.value.value)); // ie. rhs is NOT < rhs + } } catch (Exception e) { @@ -283,14 +366,30 @@ public NameValuePairList caseLessEqualExpression(TCLessEqualExpression node, Obj if (node.right instanceof TCIntegerLiteralExpression) { TCIntegerLiteralExpression rhs = (TCIntegerLiteralExpression)node.right; - nvpl.add(var.name, new IntegerValue(rhs.value.value.add(BigInteger.ONE))); // ie. rhs+1 is NOT <= rhs + + if (exists) + { + nvpl.add(var.name, new IntegerValue(rhs.value.value)); + } + else + { + nvpl.add(var.name, new IntegerValue(rhs.value.value.add(BigInteger.ONE))); // ie. rhs+1 is NOT <= rhs + } } else if (node.right instanceof TCRealLiteralExpression) { try { TCRealLiteralExpression rhs = (TCRealLiteralExpression)node.right; - nvpl.add(var.name, new RealValue(rhs.value.value.subtract(BigDecimal.ONE))); // ie. rhs+1 is NOT <= rhs + + if (exists) + { + nvpl.add(var.name, new RealValue(rhs.value.value)); + } + else + { + nvpl.add(var.name, new RealValue(rhs.value.value.add(BigDecimal.ONE))); // ie. rhs+1 is NOT <= rhs + } } catch (Exception e) { @@ -384,6 +483,7 @@ public NameValuePairList caseInSetExpression(TCInSetExpression node, Object arg) if (vartype instanceof TCNumericType) { TCNumericType numtype = (TCNumericType)vartype; + BigInteger index = (exists ? BigInteger.ONE : BigInteger.ZERO); try { @@ -393,19 +493,19 @@ public NameValuePairList caseInSetExpression(TCInSetExpression node, Object arg) break; case 1: // nat - nvpl.add(var.name, new NaturalValue(0)); + nvpl.add(var.name, new NaturalValue(index)); break; case 2: // int - nvpl.add(var.name, new IntegerValue(0)); + nvpl.add(var.name, new IntegerValue(index)); break; case 3: // rat - nvpl.add(var.name, new RationalValue(BigDecimal.ZERO)); + nvpl.add(var.name, new RationalValue(index)); break; case 4: // real - nvpl.add(var.name, new RealValue(0)); + nvpl.add(var.name, new RealValue(index)); break; default: // No idea! @@ -418,16 +518,15 @@ public NameValuePairList caseInSetExpression(TCInSetExpression node, Object arg) } } } + } + else if (node.right instanceof TCVariableExpression) + { + TCVariableExpression var = (TCVariableExpression)node.right; + TCType vartype = var.getType(); - if (node.right instanceof TCVariableExpression) + if (!(vartype instanceof TCSet1Type)) { - TCVariableExpression var = (TCVariableExpression)node.right; - TCType vartype = var.getType(); - - if (!(vartype instanceof TCSeq1Type)) - { - nvpl.add(var.name, new SeqValue()); - } + nvpl.add(var.name, new SeqValue()); } } else if (node.right instanceof TCMapDomainExpression) diff --git a/examples/quickcheck/src/main/resources/ast-tc.mappings b/examples/quickcheck/src/main/resources/ast-tc.mappings new file mode 100644 index 000000000..e54d50b74 --- /dev/null +++ b/examples/quickcheck/src/main/resources/ast-tc.mappings @@ -0,0 +1,7 @@ +########################################################################################## +# The annotation class mapping definition for the VDMJ Type Checker. See ClassMapper. +########################################################################################## + +# annotations +package annotations.ast to annotations.tc; +map ASTQuickCheckAnnotation{name, qcParam, qcTypes} to TCQuickCheckAnnotation(name, qcParam, qcTypes); diff --git a/examples/quickcheck/src/main/resources/tc-po.mappings b/examples/quickcheck/src/main/resources/tc-po.mappings new file mode 100644 index 000000000..c5d73e738 --- /dev/null +++ b/examples/quickcheck/src/main/resources/tc-po.mappings @@ -0,0 +1,8 @@ +########################################################################################## +# The class mapping definition for the VDMJ Proof Obligation Generator. See ClassMapper. +########################################################################################## + +# annotations +package annotations.tc to annotations.po; +map TCQuickCheckAnnotation{name, qcParam, qcTypes} to POQuickCheckAnnotation(name, qcParam, qcTypes); + diff --git a/examples/quickcheck/src/test/java/quickcheck/example/ExampleQCStrategy.java b/examples/quickcheck/src/test/java/quickcheck/example/ExampleQCStrategy.java index f3c09b9d9..46b63f111 100644 --- a/examples/quickcheck/src/test/java/quickcheck/example/ExampleQCStrategy.java +++ b/examples/quickcheck/src/test/java/quickcheck/example/ExampleQCStrategy.java @@ -33,6 +33,7 @@ import com.fujitsu.vdmj.in.expressions.INExpression; import com.fujitsu.vdmj.in.patterns.INBindingSetter; import com.fujitsu.vdmj.pog.ProofObligation; +import com.fujitsu.vdmj.runtime.Context; import com.fujitsu.vdmj.values.ValueList; import quickcheck.QuickCheck; @@ -77,7 +78,7 @@ public ExampleQCStrategy(List argv) @Override public String getName() { - return "example"; // Can be used with -p + return "example"; // Can be used with -s } @Override @@ -93,7 +94,7 @@ public boolean init(QuickCheck qc) } @Override - public Results getValues(ProofObligation po, INExpression exp, List binds) + public Results getValues(ProofObligation po, INExpression exp, List binds, Context ctxt) { Map values = new HashMap(); long before = System.currentTimeMillis(); @@ -115,6 +116,6 @@ public String help() @Override public boolean useByDefault() { - return false; // Not used if no -p options given + return false; // Not used if no -s options given } } diff --git a/lsp/src/main/java/vdmj/commands/AnalysisCommand.java b/lsp/src/main/java/vdmj/commands/AnalysisCommand.java index 32b0fdd60..e63c741c6 100644 --- a/lsp/src/main/java/vdmj/commands/AnalysisCommand.java +++ b/lsp/src/main/java/vdmj/commands/AnalysisCommand.java @@ -50,6 +50,14 @@ protected AnalysisCommand(String line) */ public abstract boolean notWhenRunning(); + /** + * Returns true if this command should not be executed when spec has errors or unsaved changes. + */ + public boolean notWhenDirty() + { + return false; + } + /** * Create an AnalysisCommand instance from the line passed, using the PluginRegistry. * Errors should be caught and turned into ErrorCommands, which print a message when diff --git a/lsp/src/main/java/vdmj/commands/PrintCommand.java b/lsp/src/main/java/vdmj/commands/PrintCommand.java index bbdeb8700..09abe77c9 100644 --- a/lsp/src/main/java/vdmj/commands/PrintCommand.java +++ b/lsp/src/main/java/vdmj/commands/PrintCommand.java @@ -92,6 +92,12 @@ public boolean notWhenRunning() { return true; } + + @Override + public boolean notWhenDirty() + { + return true; + } @Override public String scriptRun(DAPRequest request) throws IOException diff --git a/lsp/src/main/java/vdmj/commands/ScriptCommand.java b/lsp/src/main/java/vdmj/commands/ScriptCommand.java index ffffda27d..3ac2dc5e0 100644 --- a/lsp/src/main/java/vdmj/commands/ScriptCommand.java +++ b/lsp/src/main/java/vdmj/commands/ScriptCommand.java @@ -65,6 +65,12 @@ public boolean notWhenRunning() return true; } + @Override + public boolean notWhenDirty() + { + return true; + } + @Override public String scriptRun(DAPRequest request) throws IOException { diff --git a/lsp/src/main/java/workspace/DAPWorkspaceManager.java b/lsp/src/main/java/workspace/DAPWorkspaceManager.java index f0ed20b3c..1cffb2a36 100644 --- a/lsp/src/main/java/workspace/DAPWorkspaceManager.java +++ b/lsp/src/main/java/workspace/DAPWorkspaceManager.java @@ -77,8 +77,6 @@ import lsp.Utils; import vdmj.DAPDebugReader; import vdmj.commands.AnalysisCommand; -import vdmj.commands.PrintCommand; -import vdmj.commands.ScriptCommand; import workspace.events.DAPBeforeEvaluateEvent; import workspace.events.DAPConfigDoneEvent; import workspace.events.DAPDisconnectEvent; @@ -764,8 +762,7 @@ public DAPMessageList dapEvaluate(DAPRequest request, String expression, String // If we are about to evaluate something, check that we can execute. - if (command instanceof PrintCommand || - command instanceof ScriptCommand) + if (command.notWhenDirty()) { if (specHasErrors()) { diff --git a/lsp/src/main/java/workspace/plugins/POPluginPR.java b/lsp/src/main/java/workspace/plugins/POPluginPR.java index 3852b9c70..7154e2bfd 100644 --- a/lsp/src/main/java/workspace/plugins/POPluginPR.java +++ b/lsp/src/main/java/workspace/plugins/POPluginPR.java @@ -36,6 +36,7 @@ public class POPluginPR extends POPlugin { private POClassList poClassList; + private ProofObligationList obligationList; public POPluginPR() { @@ -47,6 +48,7 @@ protected void preCheck(CheckPrepareEvent ev) { super.preCheck(ev); poClassList = null; + obligationList = null; } @SuppressWarnings("unchecked") @@ -66,11 +68,14 @@ public boolean checkLoadedFiles(T tcList) throws Exception @Override public ProofObligationList getProofObligations() { - POAnnotation.init(); - ProofObligationList list = poClassList.getProofObligations(); - POAnnotation.close(); - list.renumber(); + if (obligationList == null) + { + POAnnotation.init(); + obligationList = poClassList.getProofObligations(); + POAnnotation.close(); + obligationList.renumber(); + } - return list; + return obligationList; } } diff --git a/lsp/src/main/java/workspace/plugins/POPluginSL.java b/lsp/src/main/java/workspace/plugins/POPluginSL.java index 647be6e9f..d6267b166 100644 --- a/lsp/src/main/java/workspace/plugins/POPluginSL.java +++ b/lsp/src/main/java/workspace/plugins/POPluginSL.java @@ -36,6 +36,7 @@ public class POPluginSL extends POPlugin { private POModuleList poModuleList; + private ProofObligationList obligationList; public POPluginSL() { @@ -47,6 +48,7 @@ public void preCheck(CheckPrepareEvent ev) { super.preCheck(ev); poModuleList = null; + obligationList = null; } @SuppressWarnings("unchecked") @@ -66,10 +68,14 @@ public boolean checkLoadedFiles(T tcList) throws Exception @Override public ProofObligationList getProofObligations() { - POAnnotation.init(); - ProofObligationList list = poModuleList.getProofObligations(); - POAnnotation.close(); - list.renumber(); - return list; + if (obligationList == null) + { + POAnnotation.init(); + obligationList = poModuleList.getProofObligations(); + POAnnotation.close(); + obligationList.renumber(); + } + + return obligationList; } } diff --git a/vdmj/documentation/UserGuide.odt b/vdmj/documentation/UserGuide.odt index dd9a741d9..88e95fa4d 100644 Binary files a/vdmj/documentation/UserGuide.odt and b/vdmj/documentation/UserGuide.odt differ diff --git a/vdmj/documentation/UserGuide.pdf b/vdmj/documentation/UserGuide.pdf index d7d712037..04d284f10 100644 Binary files a/vdmj/documentation/UserGuide.pdf and b/vdmj/documentation/UserGuide.pdf differ diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/ast/annotations/ASTAnnotation.java b/vdmj/src/main/java/com/fujitsu/vdmj/ast/annotations/ASTAnnotation.java index c06494d3d..e13af9df5 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/ast/annotations/ASTAnnotation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/ast/annotations/ASTAnnotation.java @@ -55,11 +55,6 @@ public ASTAnnotation(LexIdentifierToken name) this.name = name; } - public void setArgs(ASTExpressionList args) - { - this.args = args; - } - @Override public String toString() { @@ -76,14 +71,13 @@ protected void parseException(String message, LexLocation location) throws LexEx * round brackets. This method can be overridden in particular annotations if the * default syntax is not appropriate. */ - public ASTExpressionList parse(LexTokenReader ltr) throws LexException, ParserException + public void parse(LexTokenReader ltr) throws LexException, ParserException { - ASTExpressionList args = new ASTExpressionList(); - if (ltr.nextToken().is(Token.BRA)) { if (ltr.nextToken().isNot(Token.KET)) { + this.args = new ASTExpressionList(); ExpressionReader er = new ExpressionReader(ltr); args.add(er.readExpression()); @@ -99,8 +93,6 @@ public ASTExpressionList parse(LexTokenReader ltr) throws LexException, ParserEx parseException("Expecting ')' after annotation", ltr.getLast().location); } } - - return args; } public void astBefore(DefinitionReader reader) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INFuncInstantiationExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INFuncInstantiationExpression.java index 09bbd3157..1efa6c974 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INFuncInstantiationExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INFuncInstantiationExpression.java @@ -97,7 +97,7 @@ public Value eval(Context ctxt) for (int i=0; i< actualTypes.size(); i++) { TCType ptype = actualTypes.get(i); - List names = ptype.apply(collector, null); + List names = ptype.apply(collector, null); if (!names.isEmpty()) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INTypeBind.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INTypeBind.java index 41b87ce2f..30010f2a3 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INTypeBind.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INTypeBind.java @@ -40,17 +40,18 @@ public class INTypeBind extends INBind implements INBindingSetter { private static final long serialVersionUID = 1L; public final TCType type; - public final boolean hasTypeParams; + public final boolean hasPolymorphic; private ValueList bindValues = null; private Context bindCounterexample = null; private boolean bindPermuted = false; + private boolean bindOverride = false; public INTypeBind(INPattern pattern, TCType type) { super(pattern.location, pattern); this.type = type; - this.hasTypeParams = !type.apply(new TCParameterCollector(), null).isEmpty(); + this.hasPolymorphic = !type.apply(new TCParameterCollector(), null).isEmpty(); } @Override @@ -59,11 +60,13 @@ public void setBindValues(ValueList values) if (values == null) { bindValues = null; + bindOverride = false; } else { bindValues = new ValueList(); bindValues.addAll(values); + bindOverride = true; } } @@ -117,7 +120,7 @@ public String toString() @Override public ValueList getBindValues(Context ctxt, boolean permuted) throws ValueException { - if (bindValues != null && bindPermuted == permuted && !hasTypeParams) + if (bindOverride || (bindValues != null && bindPermuted == permuted && !hasPolymorphic)) { return bindValues; // Should be exactly the same } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/plugins/VDMJ.java b/vdmj/src/main/java/com/fujitsu/vdmj/plugins/VDMJ.java index aef5b835a..e79e36ad4 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/plugins/VDMJ.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/plugins/VDMJ.java @@ -491,7 +491,7 @@ public static boolean checkAndInitFiles() return false; } - private static int display(List messages, Classtype) + private static int display(List messages, Classtype, boolean show) { int count = 0; @@ -499,7 +499,7 @@ private static int display(List messages, Class messages, Class messages, AbstractCheckFilesEvent event) { - int nerrs = display(messages, VDMError.class); - int nwarns = display(messages, VDMWarning.class); + int nerrs = display(messages, VDMError.class, true); + int nwarns = display(messages, VDMWarning.class, warnings); ASTPlugin ast = PluginRegistry.getInstance().getPlugin("AST"); int count = ast.getCount(); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/plugins/analyses/INPlugin.java b/vdmj/src/main/java/com/fujitsu/vdmj/plugins/analyses/INPlugin.java index 1ae1542ae..1dfae561f 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/plugins/analyses/INPlugin.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/plugins/analyses/INPlugin.java @@ -79,7 +79,8 @@ abstract public class INPlugin extends AnalysisPlugin implements EventListener protected boolean startInterpreter; // eg. -e or -remote as well as -i protected boolean interactive; // eg. -i or -simulation protected String defaultName; - protected String expression; + protected String expression; // eg. -e "f(1, 2)" + protected String commandline; // eg. -cmd "qc -s fixed" protected String logfile; protected String remoteControlName; protected String remoteSimulationName; @@ -139,6 +140,7 @@ public void usage() { println("-i: run the interpreter if successfully type checked"); println("-e : evaluate and stop"); + println("-cmd : perform and stop"); println("-default : set the default module/class"); println("-pre: disable precondition checks"); println("-post: disable postcondition checks"); @@ -184,6 +186,22 @@ public void processArgs(List argv) } break; + case "-cmd": + iter.remove(); + startInterpreter = true; + interactive = false; + + if (iter.hasNext()) + { + commandline = iter.next(); + iter.remove(); + } + else + { + fail("-cmd option requires a command"); + } + break; + case "-default": iter.remove(); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/plugins/analyses/INPluginPP.java b/vdmj/src/main/java/com/fujitsu/vdmj/plugins/analyses/INPluginPP.java index 688102bdc..6bfa7436e 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/plugins/analyses/INPluginPP.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/plugins/analyses/INPluginPP.java @@ -42,6 +42,7 @@ import com.fujitsu.vdmj.mapper.ClassMapper; import com.fujitsu.vdmj.messages.Console; import com.fujitsu.vdmj.messages.VDMMessage; +import com.fujitsu.vdmj.plugins.AnalysisCommand; import com.fujitsu.vdmj.plugins.CommandReader; import com.fujitsu.vdmj.plugins.PluginRegistry; import com.fujitsu.vdmj.runtime.ClassInterpreter; @@ -146,6 +147,16 @@ else if (expression != null) { println(interpreter.execute(expression)); } + else if (commandline != null) + { + AnalysisCommand command = AnalysisCommand.parse(commandline); + String result = command.run(commandline); + + if (result != null) + { + println(result); + } + } else if (remoteClass != null) { RemoteControl remote = remoteClass.getDeclaredConstructor().newInstance(); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/plugins/analyses/INPluginSL.java b/vdmj/src/main/java/com/fujitsu/vdmj/plugins/analyses/INPluginSL.java index b7eaddf00..ac4ad048f 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/plugins/analyses/INPluginSL.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/plugins/analyses/INPluginSL.java @@ -42,6 +42,7 @@ import com.fujitsu.vdmj.mapper.ClassMapper; import com.fujitsu.vdmj.messages.Console; import com.fujitsu.vdmj.messages.VDMMessage; +import com.fujitsu.vdmj.plugins.AnalysisCommand; import com.fujitsu.vdmj.plugins.CommandReader; import com.fujitsu.vdmj.plugins.PluginRegistry; import com.fujitsu.vdmj.runtime.ContextException; @@ -147,6 +148,16 @@ else if (expression != null) // No debug thread or watcher for -e println(interpreter.execute(expression)); } + else if (commandline != null) + { + AnalysisCommand command = AnalysisCommand.parse(commandline); + String result = command.run(commandline); + + if (result != null) + { + println(result); + } + } else if (remoteClass != null) { RemoteControl remote = remoteClass.getDeclaredConstructor().newInstance(); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/plugins/analyses/POPluginPP.java b/vdmj/src/main/java/com/fujitsu/vdmj/plugins/analyses/POPluginPP.java index 44ba1616e..900537b48 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/plugins/analyses/POPluginPP.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/plugins/analyses/POPluginPP.java @@ -44,11 +44,13 @@ public class POPluginPP extends POPlugin { protected POClassList poClassList = null; + protected ProofObligationList obligationList = null; @Override protected List pogPrepare() { poClassList = null; + obligationList = null; return null; } @@ -87,11 +89,14 @@ public > T getPO() @Override public ProofObligationList getProofObligations() { - POAnnotation.init(); - ProofObligationList list = poClassList.getProofObligations(); - POAnnotation.close(); - list.renumber(); + if (obligationList == null) + { + POAnnotation.init(); + obligationList = poClassList.getProofObligations(); + POAnnotation.close(); + obligationList.renumber(); + } - return list; + return obligationList; } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/plugins/analyses/POPluginSL.java b/vdmj/src/main/java/com/fujitsu/vdmj/plugins/analyses/POPluginSL.java index 605d2480e..666bbb6e6 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/plugins/analyses/POPluginSL.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/plugins/analyses/POPluginSL.java @@ -44,11 +44,13 @@ public class POPluginSL extends POPlugin { protected POModuleList poModuleList = null; + protected ProofObligationList obligationList = null; @Override protected List pogPrepare() { poModuleList = null; + obligationList = null; return null; } @@ -87,10 +89,14 @@ public > T getPO() @Override public ProofObligationList getProofObligations() { - POAnnotation.init(); - ProofObligationList list = poModuleList.getProofObligations(); - POAnnotation.close(); - list.renumber(); - return list; + if (obligationList == null) + { + POAnnotation.init(); + obligationList = poModuleList.getProofObligations(); + POAnnotation.close(); + obligationList.renumber(); + } + + return obligationList; } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POElementsExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POElementsExpression.java index 20a9b2c34..cce3c8271 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POElementsExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POElementsExpression.java @@ -43,7 +43,7 @@ public POElementsExpression(LexLocation location, POExpression exp) @Override public String toString() { - return "(elems " + exp + ")"; + return "(elems (" + exp + "))"; } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POFuncInstantiationExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POFuncInstantiationExpression.java index 6a6a468bb..19ffb98b4 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POFuncInstantiationExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POFuncInstantiationExpression.java @@ -30,9 +30,9 @@ import com.fujitsu.vdmj.pog.POContextStack; import com.fujitsu.vdmj.pog.ProofObligationList; import com.fujitsu.vdmj.tc.types.TCFunctionType; +import com.fujitsu.vdmj.tc.types.TCType; import com.fujitsu.vdmj.tc.types.TCTypeList; import com.fujitsu.vdmj.typechecker.Environment; -import com.fujitsu.vdmj.util.Utils; public class POFuncInstantiationExpression extends POExpression { @@ -60,7 +60,22 @@ public POFuncInstantiationExpression(POExpression function, @Override public String toString() { - return "(" + function + ")[" + Utils.listToString(actualTypes) + "]"; + StringBuilder sb = new StringBuilder(); + + sb.append("("); + sb.append(function); + sb.append(")["); + String sep = ""; + + for (TCType p: actualTypes) + { + sb.append(sep); + sb.append(p.toExplicitString(location)); + sep = ", "; + } + + sb.append("]"); + return sb.toString(); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/FuncComposeObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/FuncComposeObligation.java index a71750273..161b41c1c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/FuncComposeObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/FuncComposeObligation.java @@ -35,7 +35,7 @@ public FuncComposeObligation( StringBuilder sb = new StringBuilder(); sb.append("forall arg:"); - sb.append(explicitType(exp.ltype.getFunction().parameters.get(0), exp.location)); + sb.append(explicitType(exp.rtype.getFunction().parameters.get(0), exp.location)); sb.append(" & "); if (pref2 == null || !pref2.equals("")) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/FuncPostConditionObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/FuncPostConditionObligation.java index b767d20e2..f809240ff 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/FuncPostConditionObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/FuncPostConditionObligation.java @@ -120,10 +120,10 @@ private String functionCall(POExplicitFunctionDefinition def, String addResult) sb.append("["); String sep = ""; - for (@SuppressWarnings("unused") TCType p: def.typeParams) + for (TCType p: def.typeParams) { sb.append(sep); - sb.append("?"); + sb.append(p); sep = ", "; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContext.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContext.java index ca6d28cda..04bd754ca 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContext.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContext.java @@ -29,10 +29,12 @@ import java.util.Map; import java.util.Vector; +import com.fujitsu.vdmj.po.annotations.POAnnotationList; import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.po.patterns.POPatternList; import com.fujitsu.vdmj.tc.lex.TCNameToken; import com.fujitsu.vdmj.tc.types.TCType; +import com.fujitsu.vdmj.tc.types.TCTypeList; abstract public class POContext { @@ -44,6 +46,16 @@ public String getName() return ""; // Overridden in PONameContext } + public POAnnotationList getAnnotations() + { + return null; + } + + public TCTypeList getTypeParams() + { + return null; + } + public boolean isScopeBoundary() { return false; @@ -59,14 +71,14 @@ public TCType checkType(POExpression exp) return knownTypes.get(exp); } - protected String preconditionCall(TCNameToken name, POPatternList paramPatternList, POExpression body) + protected String preconditionCall(TCNameToken name, TCTypeList typeParams, POPatternList paramPatternList, POExpression body) { List pplist = new Vector(); pplist.add(paramPatternList); - return preconditionCall(name, pplist, body); + return preconditionCall(name, typeParams, pplist, body); } - protected String preconditionCall(TCNameToken name, List paramPatternList, POExpression body) + protected String preconditionCall(TCNameToken name, TCTypeList typeParams, List paramPatternList, POExpression body) { if (body == null) { @@ -75,6 +87,21 @@ protected String preconditionCall(TCNameToken name, List paramPat StringBuilder call = new StringBuilder(); call.append(name.getPreName(name.getLocation())); + + if (typeParams != null && !typeParams.isEmpty()) + { + call.append("["); + String sep = ""; + + for (TCType param: typeParams) + { + call.append(sep); + call.append(param); + sep = ", "; + } + + call.append("]"); + } for (POPatternList plist: paramPatternList) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java index 1ec83da07..15fbfb1d0 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java @@ -27,9 +27,11 @@ import java.util.ListIterator; import java.util.Stack; +import com.fujitsu.vdmj.po.annotations.POAnnotationList; import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.po.patterns.visitors.POGetMatchingExpressionVisitor; import com.fujitsu.vdmj.tc.types.TCType; +import com.fujitsu.vdmj.tc.types.TCTypeList; @SuppressWarnings("serial") public class POContextStack extends Stack @@ -103,6 +105,36 @@ public String getObligation(String root) // Finally, we change any polymorphic types to "?" for now return result.toString().replaceAll("@\\w+", "?"); } + + public POAnnotationList getAnnotations() + { + for (POContext ctxt: this) + { + POAnnotationList annotations = ctxt.getAnnotations(); + + if (annotations != null && !annotations.isEmpty()) + { + return annotations; + } + } + + return null; + } + + public TCTypeList getTypeParams() + { + for (POContext ctxt: this) + { + TCTypeList params = ctxt.getTypeParams(); + + if (params != null && !params.isEmpty()) + { + return params; + } + } + + return null; + } private String indentNewLines(String line, String indent) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POFunctionDefinitionContext.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POFunctionDefinitionContext.java index 0baa0c915..833d16420 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POFunctionDefinitionContext.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POFunctionDefinitionContext.java @@ -27,6 +27,7 @@ import java.util.Iterator; import java.util.List; +import com.fujitsu.vdmj.po.annotations.POAnnotationList; import com.fujitsu.vdmj.po.definitions.POExplicitFunctionDefinition; import com.fujitsu.vdmj.po.definitions.POImplicitFunctionDefinition; import com.fujitsu.vdmj.po.patterns.POPattern; @@ -35,35 +36,42 @@ import com.fujitsu.vdmj.tc.lex.TCNameToken; import com.fujitsu.vdmj.tc.types.TCFunctionType; import com.fujitsu.vdmj.tc.types.TCType; +import com.fujitsu.vdmj.tc.types.TCTypeList; public class POFunctionDefinitionContext extends POContext { + public final POAnnotationList annotations; public final TCNameToken name; public final TCFunctionType deftype; public final List paramPatternList; public final boolean addPrecond; public final String precondition; + public final TCTypeList typeParams; public POFunctionDefinitionContext( POExplicitFunctionDefinition definition, boolean precond) { + this.annotations = definition.annotations; this.name = definition.name; this.deftype = definition.type; this.paramPatternList = definition.paramPatternList; this.addPrecond = precond; POGetMatchingExpressionVisitor.init(); - this.precondition = preconditionCall(name, paramPatternList, definition.precondition); + this.precondition = preconditionCall(name, definition.typeParams, paramPatternList, definition.precondition); + this.typeParams = definition.typeParams; } public POFunctionDefinitionContext( POImplicitFunctionDefinition definition, boolean precond) { + this.annotations = definition.annotations; this.name = definition.name; this.deftype = definition.type; this.addPrecond = precond; this.paramPatternList = definition.getParamPatternList(); POGetMatchingExpressionVisitor.init(); - this.precondition = preconditionCall(name, paramPatternList, definition.precondition); + this.precondition = preconditionCall(name, definition.typeParams, paramPatternList, definition.precondition); + this.typeParams = definition.typeParams; } @Override @@ -114,4 +122,16 @@ public String getContext() return sb.toString(); } + + @Override + public TCTypeList getTypeParams() + { + return typeParams; + } + + @Override + public POAnnotationList getAnnotations() + { + return annotations; + } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POFunctionResultContext.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POFunctionResultContext.java index 0bc9267d8..1aeb16ebe 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POFunctionResultContext.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POFunctionResultContext.java @@ -45,7 +45,7 @@ public POFunctionResultContext(POExplicitFunctionDefinition definition) { this.name = definition.name; this.deftype = definition.type; - this.precondition = preconditionCall(name, definition.paramPatternList, definition.precondition); + this.precondition = preconditionCall(name, definition.typeParams, definition.paramPatternList, definition.precondition); this.body = definition.body; this.implicit = false; @@ -60,7 +60,7 @@ public POFunctionResultContext(POImplicitFunctionDefinition definition) { this.name = definition.name; this.deftype = definition.type; - this.precondition = preconditionCall(name, definition.getParamPatternList(), definition.precondition); + this.precondition = preconditionCall(name, definition.typeParams, definition.getParamPatternList(), definition.precondition); this.body = definition.body; this.implicit = true; this.result = definition.result; diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POImpliesContext.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POImpliesContext.java index b4f033d93..355355ec6 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POImpliesContext.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POImpliesContext.java @@ -39,12 +39,12 @@ public POImpliesContext(POExpression precondition) public POImpliesContext(POExplicitOperationDefinition def) { - this.exp = preconditionCall(def.name, def.getParamPatternList(), def.precondition); + this.exp = preconditionCall(def.name, null, def.getParamPatternList(), def.precondition); } public POImpliesContext(POImplicitOperationDefinition def) { - this.exp = preconditionCall(def.name, def.getParamPatternList(), def.precondition); + this.exp = preconditionCall(def.name, null, def.getParamPatternList(), def.precondition); } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POOperationDefinitionContext.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POOperationDefinitionContext.java index 6663e81f0..8d4b154fa 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POOperationDefinitionContext.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POOperationDefinitionContext.java @@ -52,7 +52,7 @@ public POOperationDefinitionContext(POImplicitOperationDefinition definition, this.deftype = definition.type; this.addPrecond = precond; this.paramPatternList = definition.getParamPatternList(); - this.precondition = preconditionCall(name, paramPatternList, definition.precondition); + this.precondition = preconditionCall(name, null, paramPatternList, definition.precondition); this.stateDefinition = stateDefinition; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POStatus.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POStatus.java index 094bd931a..e3b25bf5c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POStatus.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POStatus.java @@ -26,7 +26,7 @@ public enum POStatus { - UNPROVED("Unproved"), PROVED("Proved"), TRIVIAL("Trivial"), MAYBE("Maybe"), UNCHECKED("Unchecked"); + UNPROVED("Unproved"), PROVED("Proved"), TRIVIAL("Trivial"), MAYBE("Maybe"), UNCHECKED("Unchecked"), FAILED("Failed"); private String text; 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 24ebc487c..71fc7b5f1 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java @@ -25,9 +25,11 @@ package com.fujitsu.vdmj.pog; import com.fujitsu.vdmj.lex.LexLocation; +import com.fujitsu.vdmj.po.annotations.POAnnotationList; import com.fujitsu.vdmj.po.patterns.visitors.POGetMatchingExpressionVisitor; import com.fujitsu.vdmj.tc.expressions.TCExpression; import com.fujitsu.vdmj.tc.types.TCType; +import com.fujitsu.vdmj.tc.types.TCTypeList; abstract public class ProofObligation implements Comparable { @@ -40,6 +42,8 @@ abstract public class ProofObligation implements Comparable public POStatus status; public POTrivialProof proof; public boolean isCheckable; + public TCTypeList typeParams; + public POAnnotationList annotations; private int var = 1; private TCExpression checkedExpression = null; @@ -53,6 +57,8 @@ public ProofObligation(LexLocation location, POType kind, POContextStack ctxt) this.proof = null; this.number = 0; this.isCheckable = ctxt.isCheckable(); // Set false for operation POs + this.typeParams = ctxt.getTypeParams(); + this.annotations = ctxt.getAnnotations(); if (!isCheckable) { @@ -66,6 +72,11 @@ public String getValue() { return value; } + + public void setStatus(POStatus status) + { + this.status = status; + } @Override public String toString() diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/TotalFunctionObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/TotalFunctionObligation.java index 968d42779..44d890b2d 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/TotalFunctionObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/TotalFunctionObligation.java @@ -31,6 +31,7 @@ import com.fujitsu.vdmj.po.patterns.POPattern; import com.fujitsu.vdmj.po.patterns.POPatternList; import com.fujitsu.vdmj.tc.types.TCFunctionType; +import com.fujitsu.vdmj.tc.types.TCType; public class TotalFunctionObligation extends ProofObligation { @@ -54,10 +55,10 @@ private String getContext(String name, POExplicitFunctionDefinition def) { fapply.append("["); - for (int p=0; p < def.typeParams.size(); p++) + for (TCType ptype: def.typeParams) { fapply.append(sep); - fapply.append("?"); + fapply.append(ptype.toString()); sep = ", "; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/syntax/SyntaxReader.java b/vdmj/src/main/java/com/fujitsu/vdmj/syntax/SyntaxReader.java index e11466ae9..de6d397c0 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/syntax/SyntaxReader.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/syntax/SyntaxReader.java @@ -33,7 +33,6 @@ import com.fujitsu.vdmj.Settings; import com.fujitsu.vdmj.ast.annotations.ASTAnnotation; import com.fujitsu.vdmj.ast.annotations.ASTAnnotationList; -import com.fujitsu.vdmj.ast.expressions.ASTExpressionList; import com.fujitsu.vdmj.ast.lex.LexCommentList; import com.fujitsu.vdmj.ast.lex.LexIdentifierToken; import com.fujitsu.vdmj.ast.lex.LexNameToken; @@ -408,8 +407,7 @@ private ASTAnnotation readAnnotation(LexTokenReader ltr) throws LexException, Pa { LexIdentifierToken name = (LexIdentifierToken)ltr.getLast(); ASTAnnotation annotation = loadAnnotation(name); - ASTExpressionList args = annotation.parse(ltr); - annotation.setArgs(args); + annotation.parse(ltr); return annotation; } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/visitors/TCDependencyDefinitionVisitor.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/visitors/TCDependencyDefinitionVisitor.java index 97e9bd775..e1999df92 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/visitors/TCDependencyDefinitionVisitor.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/visitors/TCDependencyDefinitionVisitor.java @@ -65,7 +65,7 @@ protected void setVisitors() definitionVisitor = TCDependencyDefinitionVisitor.this; expressionVisitor = new TCDependencyExpressionVisitor(this); statementVisitor = new TCDependencyStatementVisitor(this); - typeVisitor = new TCDependencyTypeVisitor(this); + typeVisitor = new TCDependencyTypeVisitor(); bindVisitor = new TCDependencyBindVisitor(this); multiBindVisitor = new TCDependencyMultipleBindVisitor(this); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/visitors/TCFreeVariableDefinitionVisitor.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/visitors/TCFreeVariableDefinitionVisitor.java index fd6b67134..05da55d87 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/visitors/TCFreeVariableDefinitionVisitor.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/visitors/TCFreeVariableDefinitionVisitor.java @@ -61,7 +61,7 @@ protected void setVisitors() expressionVisitor = new TCFreeVariableExpressionVisitor(this); statementVisitor = new TCFreeVariableStatementVisitor(this); patternVisitor = new TCFreeVariablePatternVisitor(this); - typeVisitor = new TCFreeVariableTypeVisitor(this); + typeVisitor = new TCFreeVariableTypeVisitor(); bindVisitor = new TCFreeVariableBindVisitor(this); multiBindVisitor = new TCFreeVariableMultipleBindVisitor(this); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/expressions/visitors/TCQualifiedDefinitionFinder.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/expressions/visitors/TCQualifiedDefinitionFinder.java index 5846a6705..7b6175dc8 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/expressions/visitors/TCQualifiedDefinitionFinder.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/expressions/visitors/TCQualifiedDefinitionFinder.java @@ -97,7 +97,7 @@ public TCDefinitionList caseIsExpression(TCIsExpression node, Environment env) { TCVariableExpression exp = (TCVariableExpression)node.test; // Lookup with any name type to avoid scope errors, but test NAMES below. - TCDefinition existing = env.findName(exp.name, NameScope.NAMESANDSTATE); + TCDefinition existing = env.findName(exp.name, NameScope.NAMESANDANYSTATE); if (existing != null && existing.nameScope.matches(NameScope.NAMES)) { @@ -133,7 +133,7 @@ public TCDefinitionList caseNotEqualExpression(TCNotEqualExpression node, Enviro { TCVariableExpression var = (TCVariableExpression)node.left; // Lookup with any name type to avoid scope errors, but test NAMES below. - TCDefinition existing = env.findName(var.name, NameScope.NAMESANDSTATE); + TCDefinition existing = env.findName(var.name, NameScope.NAMESANDANYSTATE); if (existing != null && existing.nameScope.matches(NameScope.NAMES) && existing.getType() instanceof TCOptionalType) @@ -156,7 +156,7 @@ public TCDefinitionList caseEqualsExpression(TCEqualsExpression node, Environmen { TCVariableExpression var = (TCVariableExpression)node.left; // Lookup with any name type to avoid scope errors, but test NAMES below. - TCDefinition existing = env.findName(var.name, NameScope.NAMESANDSTATE); + TCDefinition existing = env.findName(var.name, NameScope.NAMESANDANYSTATE); if (existing != null && existing.nameScope.matches(NameScope.NAMES)) { @@ -177,7 +177,7 @@ public TCDefinitionList caseInSetExpression(TCInSetExpression node, Environment { TCVariableExpression var = (TCVariableExpression)node.left; // Lookup with any name type to avoid scope errors, but test NAMES below. - TCDefinition existing = env.findName(var.name, NameScope.NAMESANDSTATE); + TCDefinition existing = env.findName(var.name, NameScope.NAMESANDANYSTATE); if (existing != null && existing.nameScope.matches(NameScope.NAMES)) { @@ -202,7 +202,7 @@ public TCDefinitionList caseEquivalentExpression(TCEquivalentExpression node, En { TCVariableExpression var = (TCVariableExpression)node.left; // Lookup with any name type to avoid scope errors, but test NAMES below. - TCDefinition existing = env.findName(var.name, NameScope.NAMESANDSTATE); + TCDefinition existing = env.findName(var.name, NameScope.NAMESANDANYSTATE); if (existing != null && existing.nameScope.matches(NameScope.NAMES)) { @@ -223,7 +223,7 @@ public TCDefinitionList caseSubsetExpression(TCSubsetExpression node, Environmen { TCVariableExpression var = (TCVariableExpression)node.left; // Lookup with any name type to avoid scope errors, but test NAMES below. - TCDefinition existing = env.findName(var.name, NameScope.NAMESANDSTATE); + TCDefinition existing = env.findName(var.name, NameScope.NAMESANDANYSTATE); if (existing != null && existing.nameScope.matches(NameScope.NAMES)) { @@ -248,7 +248,7 @@ public TCDefinitionList caseProperSubsetExpression(TCProperSubsetExpression node { TCVariableExpression var = (TCVariableExpression)node.left; // Lookup with any name type to avoid scope errors, but test NAMES below. - TCDefinition existing = env.findName(var.name, NameScope.NAMESANDSTATE); + TCDefinition existing = env.findName(var.name, NameScope.NAMESANDANYSTATE); if (existing != null && existing.nameScope.matches(NameScope.NAMES)) { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/visitors/TCDependencyTypeVisitor.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/visitors/TCDependencyTypeVisitor.java index b6d65e9ec..ac850ecfe 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/visitors/TCDependencyTypeVisitor.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/visitors/TCDependencyTypeVisitor.java @@ -24,7 +24,6 @@ package com.fujitsu.vdmj.tc.types.visitors; -import com.fujitsu.vdmj.tc.TCVisitorSet; import com.fujitsu.vdmj.tc.expressions.EnvTriple; import com.fujitsu.vdmj.tc.lex.TCNameSet; import com.fujitsu.vdmj.tc.lex.TCNameToken; @@ -35,9 +34,9 @@ public class TCDependencyTypeVisitor extends TCLeafTypeVisitor { - public TCDependencyTypeVisitor(TCVisitorSet visitors) + public TCDependencyTypeVisitor() { - visitorSet = visitors; + // No visitor set } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/visitors/TCFreeVariableTypeVisitor.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/visitors/TCFreeVariableTypeVisitor.java index e084d9498..908137399 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/visitors/TCFreeVariableTypeVisitor.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/visitors/TCFreeVariableTypeVisitor.java @@ -24,7 +24,6 @@ package com.fujitsu.vdmj.tc.types.visitors; -import com.fujitsu.vdmj.tc.TCVisitorSet; import com.fujitsu.vdmj.tc.lex.TCNameSet; import com.fujitsu.vdmj.tc.lex.TCNameToken; import com.fujitsu.vdmj.tc.types.TCType; @@ -32,10 +31,9 @@ public class TCFreeVariableTypeVisitor extends TCLeafTypeVisitor { - public TCFreeVariableTypeVisitor(TCVisitorSet visitors) + public TCFreeVariableTypeVisitor() { - assert visitors != null : "Visitor set cannot be null"; - visitorSet = visitors; + // No visitor set } @Override diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/visitors/TCLeafTypeVisitor.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/visitors/TCLeafTypeVisitor.java index 478522b4c..dccaf60ab 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/visitors/TCLeafTypeVisitor.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/visitors/TCLeafTypeVisitor.java @@ -26,7 +26,6 @@ import java.util.Collection; -import com.fujitsu.vdmj.tc.TCVisitorSet; import com.fujitsu.vdmj.tc.types.TCBracketType; import com.fujitsu.vdmj.tc.types.TCField; import com.fujitsu.vdmj.tc.types.TCFunctionType; @@ -51,20 +50,13 @@ */ public abstract class TCLeafTypeVisitor, S> extends TCTypeVisitor { - protected TCVisitorSet visitorSet = new TCVisitorSet() - { - @Override - protected void setVisitors() - { - typeVisitor = TCLeafTypeVisitor.this; - } - - @Override - protected C newCollection() - { - return TCLeafTypeVisitor.this.newCollection(); - } - }; + /** + * There is no visitor set here, because the TCType leaf visitor does not call out to any + * other grammatical group (like expVisitor etc). Also, since TCTypes are not mapped + * beyond the TC tree, you cannot use (say) an INVisitorSet here anyway. + */ + + // No visitorSet... /** * We have to collect the nodes that have already been visited since types can be recursive, diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/visitors/TCParameterCollector.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/visitors/TCParameterCollector.java index 0e3140ead..a459f1905 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/visitors/TCParameterCollector.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/visitors/TCParameterCollector.java @@ -35,30 +35,30 @@ * that are contained in the TCType being visited. This is used by the * TCTypeComparator. */ -public class TCParameterCollector extends TCLeafTypeVisitor, Object> +public class TCParameterCollector extends TCLeafTypeVisitor, Object> { public TCParameterCollector() { - // default visitorSet + // No visitorSet } @Override - public List caseParameterType(TCParameterType node, Object arg) + public List caseParameterType(TCParameterType node, Object arg) { - List all = newCollection(); - all.add("@" + node.name); + List all = newCollection(); + all.add(node); return all; } @Override - public List caseType(TCType node, Object arg) + public List caseType(TCType node, Object arg) { return newCollection(); } @Override - protected List newCollection() + protected List newCollection() { - return new Vector(); + return new Vector(); } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/visitors/TCUnresolvedTypeFinder.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/visitors/TCUnresolvedTypeFinder.java index 89b8459ac..d97eb65f9 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/visitors/TCUnresolvedTypeFinder.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/visitors/TCUnresolvedTypeFinder.java @@ -33,7 +33,7 @@ public class TCUnresolvedTypeFinder extends TCLeafTypeVisitor tstr = to.apply(new TCParameterCollector(), null); + TCParameterType fstr = from.apply(new TCParameterCollector(), null).get(0); + List tstr = to.apply(new TCParameterCollector(), null); if (tstr.contains(fstr) && !(to instanceof TCParameterType)) { @@ -555,8 +555,8 @@ else if (to instanceof TCVoidReturnType) } else if (to instanceof TCParameterType) { - String tstr = to.apply(new TCParameterCollector(), null).get(0); - List fstr = from.apply(new TCParameterCollector(), null); + TCParameterType tstr = to.apply(new TCParameterCollector(), null).get(0); + List fstr = from.apply(new TCParameterCollector(), null); if (fstr.contains(tstr) && !(from instanceof TCParameterType)) {