diff --git a/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java b/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java index 41349510c..e460d48c6 100644 --- a/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java +++ b/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java @@ -48,6 +48,7 @@ public class QuickCheckCommand extends AnalysisCommand { private final static String CMD = "quickcheck [-?|-help][-q][-t ][-s ]* [-]* []"; + private final static String SHORT = "quickcheck [-help][][]"; private final static String USAGE = "Usage: " + CMD; public QuickCheckCommand(String line) @@ -224,6 +225,6 @@ public String run(String line) public static void help() { - println("quickcheck [-?|-help][-p ]* [] [] - lightweight PO verification"); + println(SHORT + " - lightweight PO verification"); } } diff --git a/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckLSPCommand.java b/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckLSPCommand.java index 3039ed16f..03d917e0d 100644 --- a/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckLSPCommand.java +++ b/examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckLSPCommand.java @@ -44,6 +44,7 @@ public class QuickCheckLSPCommand extends AnalysisCommand implements InitRunnable, ScriptRunnable { public final static String CMD = "quickcheck [-?|-help][-q][-t ][-s ]* [-]* []"; + public final static String SHORT = "quickcheck [-help][][]"; private final static String USAGE = "Usage: " + CMD; private List poList = new Vector(); diff --git a/examples/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java b/examples/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java index 2af014dec..a2d5d8e29 100644 --- a/examples/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java +++ b/examples/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java @@ -55,11 +55,11 @@ public void init() @Override public void setServerCapabilities(JSONObject capabilities) { - JSONObject experimental = capabilities.get("experimental"); + JSONObject provider = capabilities.getPath("experimental.proofObligationProvider"); - if (experimental != null) + if (provider != null) { - experimental.put("quickCheckProvider", true); + provider.put("quickCheckProvider", true); } } @@ -79,6 +79,6 @@ public AnalysisCommand getCommand(String line) @Override public HelpList getCommandHelp() { - return new HelpList("quickcheck [-p ]* [] [] - lightweight PO verification"); + return new HelpList(QuickCheckLSPCommand.SHORT + " - lightweight PO verification"); } } diff --git a/examples/quickcheck/src/main/java/quickcheck/visitors/TrivialQCVisitor.java b/examples/quickcheck/src/main/java/quickcheck/visitors/TrivialQCVisitor.java index 0f2bf1fb9..fcee029b5 100644 --- a/examples/quickcheck/src/main/java/quickcheck/visitors/TrivialQCVisitor.java +++ b/examples/quickcheck/src/main/java/quickcheck/visitors/TrivialQCVisitor.java @@ -278,7 +278,7 @@ public Boolean caseExpression(TCExpression node, Stack truths) { if (truths.contains(node)) { - evaluated.add(node.toString()); // This truth was used + evaluated.add(Utils.deBracketed(node)); // This truth was used return true; } else diff --git a/lsp/src/main/java/workspace/plugins/POPlugin.java b/lsp/src/main/java/workspace/plugins/POPlugin.java index e23bb40b3..3654fa280 100644 --- a/lsp/src/main/java/workspace/plugins/POPlugin.java +++ b/lsp/src/main/java/workspace/plugins/POPlugin.java @@ -34,6 +34,7 @@ import com.fujitsu.vdmj.messages.VDMWarning; import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; +import com.fujitsu.vdmj.runtime.Context; import json.JSONArray; import json.JSONObject; @@ -96,7 +97,7 @@ public void setServerCapabilities(JSONObject capabilities) if (experimental != null) { - experimental.put("proofObligationProvider", true); + experimental.put("proofObligationProvider", new JSONObject()); } } @@ -139,6 +140,8 @@ protected void preCheck(CheckPrepareEvent event) abstract public ProofObligationList getProofObligations(); + abstract protected JSONObject getLaunch(ProofObligation po, Context ctxt); + protected JSONArray splitPO(String value) { String[] parts = value.trim().split("\\n\\s+"); @@ -199,7 +202,16 @@ else if (file.isDirectory()) if (!po.counterexample.isEmpty()) { - json.put("counterexample", Utils.contextToJSON(po.counterexample)); + JSONObject cexample = new JSONObject(); + cexample.put("variables", Utils.contextToJSON(po.counterexample)); + JSONObject launch = getLaunch(po, po.counterexample); + + if (launch != null) + { + cexample.put("launch", launch); + } + + json.put("counterexample", cexample); StringBuilder sb = new StringBuilder(); sb.append("PO #"); @@ -207,11 +219,25 @@ else if (file.isDirectory()) sb.append(" counterexample: "); sb.append(po.counterexample.toStringLine()); messages.add(new VDMWarning(9000, sb.toString(), po.location)); + + if (po.message != null) // Add any message as a warning too + { + messages.add(new VDMWarning(9000, po.message, po.location)); + } } if (!po.witness.isEmpty()) { - json.put("witness", Utils.contextToJSON(po.witness)); + JSONObject witness = new JSONObject(); + witness.put("variables", Utils.contextToJSON(po.witness)); + JSONObject launch = getLaunch(po, po.witness); + + if (launch != null) + { + witness.put("launch", launch); + } + + json.put("witness", witness); } if (po.provedBy != null) diff --git a/lsp/src/main/java/workspace/plugins/POPluginPR.java b/lsp/src/main/java/workspace/plugins/POPluginPR.java index 7154e2bfd..3de772b25 100644 --- a/lsp/src/main/java/workspace/plugins/POPluginPR.java +++ b/lsp/src/main/java/workspace/plugins/POPluginPR.java @@ -29,8 +29,11 @@ import com.fujitsu.vdmj.po.PONode; import com.fujitsu.vdmj.po.annotations.POAnnotation; import com.fujitsu.vdmj.po.definitions.POClassList; +import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; +import com.fujitsu.vdmj.runtime.Context; +import json.JSONObject; import workspace.events.CheckPrepareEvent; public class POPluginPR extends POPlugin @@ -78,4 +81,11 @@ public ProofObligationList getProofObligations() return obligationList; } + + @Override + protected JSONObject getLaunch(ProofObligation po, Context ctxt) + { + // TODO More complex than SL as we have to think about constructors... + return null; + } } diff --git a/lsp/src/main/java/workspace/plugins/POPluginSL.java b/lsp/src/main/java/workspace/plugins/POPluginSL.java index d6267b166..5bf489406 100644 --- a/lsp/src/main/java/workspace/plugins/POPluginSL.java +++ b/lsp/src/main/java/workspace/plugins/POPluginSL.java @@ -28,9 +28,21 @@ import com.fujitsu.vdmj.mapper.Mappable; import com.fujitsu.vdmj.po.PONode; import com.fujitsu.vdmj.po.annotations.POAnnotation; +import com.fujitsu.vdmj.po.definitions.PODefinition; +import com.fujitsu.vdmj.po.definitions.POExplicitFunctionDefinition; +import com.fujitsu.vdmj.po.definitions.POImplicitFunctionDefinition; +import com.fujitsu.vdmj.po.definitions.POTypeDefinition; import com.fujitsu.vdmj.po.modules.POModuleList; +import com.fujitsu.vdmj.po.patterns.POPattern; +import com.fujitsu.vdmj.po.patterns.POPatternList; +import com.fujitsu.vdmj.po.patterns.visitors.POGetMatchingConstantVisitor; +import com.fujitsu.vdmj.po.patterns.visitors.PORemoveIgnoresVisitor; +import com.fujitsu.vdmj.po.types.POPatternListTypePair; +import com.fujitsu.vdmj.pog.ProofObligation; import com.fujitsu.vdmj.pog.ProofObligationList; +import com.fujitsu.vdmj.runtime.Context; +import json.JSONObject; import workspace.events.CheckPrepareEvent; public class POPluginSL extends POPlugin @@ -78,4 +90,108 @@ public ProofObligationList getProofObligations() return obligationList; } + + @Override + protected JSONObject getLaunch(ProofObligation po, Context ctxt) + { + PODefinition def = po.definition; + JSONObject result = null; + + if (def instanceof POExplicitFunctionDefinition) + { + POExplicitFunctionDefinition efd = (POExplicitFunctionDefinition)def; + result = launchExplicitFunction(po, efd, ctxt); + } + else if (def instanceof POImplicitFunctionDefinition) + { + POImplicitFunctionDefinition ifd = (POImplicitFunctionDefinition)def; + StringBuilder callString = new StringBuilder(); + callString.append("("); + String sep = ""; + PORemoveIgnoresVisitor.init(); + + for (POPatternListTypePair pl: ifd.parameterPatterns) + { + for (POPattern p: pl.patterns) + { + String match = paramMatch(p.removeIgnorePatterns(), ctxt); + + if (match == null) + { + return null; // Can't match some params + } + + callString.append(sep); + callString.append(match); + sep = ", "; + } + } + + callString.append(")"); + + result = new JSONObject( + "name", "PO #" + po.number + " counterexample", + "type", "vdm", + "request", "launch", + "noDebug", false, + "defaultName", def.name.getModule(), + "command", "print " + def.name.getName() + callString + ); + } + else if (def instanceof POTypeDefinition) + { + POTypeDefinition td = (POTypeDefinition)def; + + if (td.invdef != null) + { + result = launchExplicitFunction(po, td.invdef, ctxt); + } + } + + return result; + } + + private JSONObject launchExplicitFunction(ProofObligation po, POExplicitFunctionDefinition efd, Context ctxt) + { + StringBuilder callString = new StringBuilder(); + PORemoveIgnoresVisitor.init(); + + for (POPatternList pl: efd.paramPatternList) + { + callString.append("("); + String sep = ""; + + for (POPattern p: pl) + { + String match = paramMatch(p.removeIgnorePatterns(), ctxt); + + if (match == null) + { + return null; // Can't match some params + } + + callString.append(sep); + callString.append(match); + sep = ", "; + } + + callString.append(")"); + } + + return new JSONObject( + "name", "PO #" + po.number + " counterexample", + "type", "vdm", + "request", "launch", + "noDebug", false, + "defaultName", efd.name.getModule(), + "command", "print " + efd.name.getName() + callString + ); + } + + private String paramMatch(POPattern p, Context ctxt) + { + POGetMatchingConstantVisitor visitor = new POGetMatchingConstantVisitor(); + String result = p.apply(visitor, ctxt); + return visitor.hasFailed() ? null : result; + } } 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 51544502d..4e73bf093 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 @@ -160,7 +160,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment { for (PODefinitionList loop: recursive) { - obligations.add(new RecursiveObligation(loop, this, ctxt)); + obligations.add(new RecursiveObligation(location, loop, this, ctxt)); } } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/POGetMatchingConstantVisitor.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/POGetMatchingConstantVisitor.java new file mode 100644 index 000000000..b27666152 --- /dev/null +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/POGetMatchingConstantVisitor.java @@ -0,0 +1,257 @@ +/******************************************************************************* + * + * 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 com.fujitsu.vdmj.po.patterns.visitors; + +import com.fujitsu.vdmj.po.patterns.POBooleanPattern; +import com.fujitsu.vdmj.po.patterns.POCharacterPattern; +import com.fujitsu.vdmj.po.patterns.POConcatenationPattern; +import com.fujitsu.vdmj.po.patterns.POExpressionPattern; +import com.fujitsu.vdmj.po.patterns.POIdentifierPattern; +import com.fujitsu.vdmj.po.patterns.POIgnorePattern; +import com.fujitsu.vdmj.po.patterns.POIntegerPattern; +import com.fujitsu.vdmj.po.patterns.POMapPattern; +import com.fujitsu.vdmj.po.patterns.POMapUnionPattern; +import com.fujitsu.vdmj.po.patterns.POMapletPattern; +import com.fujitsu.vdmj.po.patterns.PONilPattern; +import com.fujitsu.vdmj.po.patterns.POObjectPattern; +import com.fujitsu.vdmj.po.patterns.POPattern; +import com.fujitsu.vdmj.po.patterns.POQuotePattern; +import com.fujitsu.vdmj.po.patterns.PORealPattern; +import com.fujitsu.vdmj.po.patterns.PORecordPattern; +import com.fujitsu.vdmj.po.patterns.POSeqPattern; +import com.fujitsu.vdmj.po.patterns.POSetPattern; +import com.fujitsu.vdmj.po.patterns.POStringPattern; +import com.fujitsu.vdmj.po.patterns.POTuplePattern; +import com.fujitsu.vdmj.po.patterns.POUnionPattern; +import com.fujitsu.vdmj.runtime.Context; +import com.fujitsu.vdmj.values.Value; + +/** + * This is used during the generation of PO counterexample launches. Given a pattern + * like mk_(a, b) and a Context that contains a=1 and b={1,2,3}, the visitor produces + * a String "mk_(1, {1,2,3})" and hasFailed returns false. + * + * Some patterns cannot be matched or the Context may not contain values, then + * hasFailed() is true. + */ +public class POGetMatchingConstantVisitor extends POPatternVisitor +{ + private boolean failed = false; + + public boolean hasFailed() + { + return failed; + } + + @Override + public String casePattern(POPattern node, Context arg) + { + throw new RuntimeException("Missing POGetMatchingConstantVisitor method!"); + } + + @Override + public String caseBooleanPattern(POBooleanPattern node, Context arg) + { + return node.value.toString(); + } + + @Override + public String caseCharacterPattern(POCharacterPattern node, Context arg) + { + return node.value.toString(); + } + + @Override + public String caseConcatenationPattern(POConcatenationPattern node, Context arg) + { + return node.left.apply(this, arg) + " ^ " + node.right.apply(this, arg); + } + + @Override + public String caseExpressionPattern(POExpressionPattern node, Context arg) + { + return node.exp.toString(); + } + + @Override + public String caseIdentifierPattern(POIdentifierPattern node, Context arg) + { + Value v = arg.get(node.name); + + if (v == null) + { + failed = true; + return "?"; + } + else + { + return v.toString(); + } + } + + @Override + public String caseIgnorePattern(POIgnorePattern node, Context arg) + { + failed = true; + return "?"; + } + + @Override + public String caseIntegerPattern(POIntegerPattern node, Context arg) + { + return node.value.toString(); + } + + @Override + public String caseMapPattern(POMapPattern node, Context arg) + { + StringBuilder sb = new StringBuilder("{"); + String sep = ""; + + for (POMapletPattern p: node.maplets) + { + sb.append(sep); + sb.append(p.from.apply(this, arg)); + sb.append(" |-> "); + sb.append(p.to.apply(this, arg)); + } + + sb.append("}"); + return sb.toString(); + } + + @Override + public String caseMapUnionPattern(POMapUnionPattern node, Context arg) + { + return node.left.apply(this, arg) + " munion " + node.right.apply(this, arg); + } + + @Override + public String caseNilPattern(PONilPattern node, Context arg) + { + return "nil"; + } + + @Override + public String caseObjectPattern(POObjectPattern node, Context arg) + { + failed = true; + return "?"; + } + + @Override + public String caseQuotePattern(POQuotePattern node, Context arg) + { + return node.value.toString(); + } + + @Override + public String caseRealPattern(PORealPattern node, Context arg) + { + return node.value.toString(); + } + + @Override + public String caseRecordPattern(PORecordPattern node, Context arg) + { + StringBuilder sb = new StringBuilder("mk_"); + sb.append(node.type.toExplicitString(node.location)); + sb.append("("); + String sep = ""; + + for (POPattern p: node.plist) + { + sb.append(sep); + sb.append(p.apply(this, arg)); + sep = ", "; + } + + sb.append(")"); + return sb.toString(); + } + + @Override + public String caseSeqPattern(POSeqPattern node, Context arg) + { + StringBuilder sb = new StringBuilder("["); + String sep = ""; + + for (POPattern p: node.plist) + { + sb.append(sep); + sb.append(p.apply(this, arg)); + sep = ", "; + } + + sb.append("]"); + return sb.toString(); + } + + @Override + public String caseSetPattern(POSetPattern node, Context arg) + { + StringBuilder sb = new StringBuilder("{"); + String sep = ""; + + for (POPattern p: node.plist) + { + sb.append(sep); + sb.append(p.apply(this, arg)); + sep = ", "; + } + + sb.append("}"); + return sb.toString(); + } + + @Override + public String caseStringPattern(POStringPattern node, Context arg) + { + return node.value.toString(); + } + + @Override + public String caseTuplePattern(POTuplePattern node, Context arg) + { + StringBuilder sb = new StringBuilder("mk_("); + String sep = ""; + + for (POPattern p: node.plist) + { + sb.append(sep); + sb.append(p.apply(this, arg)); + sep = ", "; + } + + sb.append(")"); + return sb.toString(); + } + + @Override + public String caseUnionPattern(POUnionPattern node, Context arg) + { + return node.left.apply(this, arg) + " union " + node.right.apply(this, arg); + } +} diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/PORemoveIgnoresVisitor.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/PORemoveIgnoresVisitor.java index 21747d1f6..35e09fc72 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/PORemoveIgnoresVisitor.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/po/patterns/visitors/PORemoveIgnoresVisitor.java @@ -103,7 +103,7 @@ public POPattern caseIgnorePattern(POIgnorePattern node, Object arg) // Generate a new "any" name for use during PO generation. The name // must be unique for the pattern instance. - TCNameToken anyName = new TCNameToken(node.location, "", "$any" + var++); + TCNameToken anyName = new TCNameToken(node.location, node.location.module, "$any" + var++); return new POIdentifierPattern(anyName); } 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 81e5ddc26..b550f6c2c 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContext.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContext.java @@ -30,6 +30,7 @@ import java.util.Vector; import com.fujitsu.vdmj.po.annotations.POAnnotationList; +import com.fujitsu.vdmj.po.definitions.PODefinition; import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.po.patterns.POPatternList; import com.fujitsu.vdmj.tc.lex.TCNameToken; @@ -115,4 +116,9 @@ protected String preconditionCall(TCNameToken name, TCTypeList typeParams, List< return call.toString(); } + + public PODefinition getDefinition() + { + return null; + } } 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 417b5c4e0..69f586dc2 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java @@ -28,6 +28,7 @@ import java.util.Stack; import com.fujitsu.vdmj.po.annotations.POAnnotationList; +import com.fujitsu.vdmj.po.definitions.PODefinition; import com.fujitsu.vdmj.po.expressions.POExpression; import com.fujitsu.vdmj.po.patterns.visitors.POGetMatchingExpressionVisitor; import com.fujitsu.vdmj.tc.types.TCType; @@ -120,6 +121,21 @@ public POAnnotationList getAnnotations() return null; } + public PODefinition getDefinition() + { + for (POContext ctxt: this) + { + PODefinition definition = ctxt.getDefinition(); + + if (definition != null) + { + return definition; + } + } + + return null; + } + public boolean isExistential() { for (POContext ctxt: this) 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 75ef2a726..3d7bd1392 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POFunctionDefinitionContext.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POFunctionDefinitionContext.java @@ -28,6 +28,7 @@ import java.util.List; import com.fujitsu.vdmj.po.annotations.POAnnotationList; +import com.fujitsu.vdmj.po.definitions.PODefinition; import com.fujitsu.vdmj.po.definitions.POExplicitFunctionDefinition; import com.fujitsu.vdmj.po.definitions.POImplicitFunctionDefinition; import com.fujitsu.vdmj.po.patterns.POPattern; @@ -41,6 +42,7 @@ public class POFunctionDefinitionContext extends POContext { + public final PODefinition definition; public final POAnnotationList annotations; public final TCNameToken name; public final TCFunctionType deftype; @@ -52,6 +54,7 @@ public class POFunctionDefinitionContext extends POContext public POFunctionDefinitionContext( POExplicitFunctionDefinition definition, boolean precond) { + this.definition = definition; this.annotations = definition.annotations; this.name = definition.name; this.deftype = definition.type; @@ -65,6 +68,7 @@ public POFunctionDefinitionContext( public POFunctionDefinitionContext( POImplicitFunctionDefinition definition, boolean precond) { + this.definition = definition; this.annotations = definition.annotations; this.name = definition.name; this.deftype = definition.type; @@ -137,4 +141,10 @@ public POAnnotationList getAnnotations() { return annotations; } + + @Override + public PODefinition getDefinition() + { + return definition; + } } 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 23126bd1f..7758370aa 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java @@ -26,6 +26,7 @@ import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.annotations.POAnnotationList; +import com.fujitsu.vdmj.po.definitions.PODefinition; import com.fujitsu.vdmj.po.patterns.visitors.POGetMatchingExpressionVisitor; import com.fujitsu.vdmj.runtime.Context; import com.fujitsu.vdmj.tc.expressions.TCExpression; @@ -41,6 +42,7 @@ abstract public class ProofObligation implements Comparable public int number; public String value; public POStatus status; + public PODefinition definition; public boolean isCheckable; public TCTypeList typeParams; public POAnnotationList annotations; @@ -59,6 +61,7 @@ public ProofObligation(LexLocation location, POType kind, POContextStack ctxt) this.kind = kind; this.name = ctxt.getName(); this.status = POStatus.UNPROVED; + this.definition = ctxt.getDefinition(); this.number = 0; this.isCheckable = ctxt.isCheckable(); // Set false for operation POs this.typeParams = ctxt.getTypeParams(); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/RecursiveObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/RecursiveObligation.java index 598165790..9386d8984 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/RecursiveObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/RecursiveObligation.java @@ -24,6 +24,7 @@ package com.fujitsu.vdmj.pog; +import com.fujitsu.vdmj.lex.LexLocation; import com.fujitsu.vdmj.po.definitions.PODefinition; import com.fujitsu.vdmj.po.definitions.PODefinitionList; import com.fujitsu.vdmj.po.definitions.POExplicitFunctionDefinition; @@ -62,9 +63,9 @@ public RecursiveObligation( value = ctxt.getObligation(greater(measureLexical, lhs, rhs)); } - public RecursiveObligation(PODefinitionList defs, POApplyExpression apply, POContextStack ctxt) + public RecursiveObligation(LexLocation location, PODefinitionList defs, POApplyExpression apply, POContextStack ctxt) { - super(defs.get(0).location, POType.RECURSIVE, ctxt); + super(location, POType.RECURSIVE, ctxt); int measureLexical = getLex(getMeasureDef(defs.get(0))); String lhs = getLHS(defs.get(0)); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/SatisfiabilityObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/SatisfiabilityObligation.java index b97f98724..ff83f4b83 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/SatisfiabilityObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/SatisfiabilityObligation.java @@ -43,6 +43,7 @@ public class SatisfiabilityObligation extends ProofObligation public SatisfiabilityObligation(POImplicitFunctionDefinition func, POContextStack ctxt) { super(func.location, POType.FUNC_SATISFIABILITY, ctxt); + this.definition = func; StringBuilder sb = new StringBuilder(); if (func.predef != null) @@ -110,6 +111,7 @@ public SatisfiabilityObligation(POImplicitOperationDefinition op, public SatisfiabilityObligation(POTypeDefinition typedef, POContextStack ctxt) { super(typedef.location, POType.INV_SATISFIABILITY, ctxt); + this.definition = typedef.invdef; StringBuilder sb = new StringBuilder(); sb.append("exists "); @@ -136,6 +138,7 @@ public SatisfiabilityObligation(POTypeDefinition typedef, POContextStack ctxt) public SatisfiabilityObligation(POStateDefinition statedef, POContextStack ctxt) { super(statedef.location, POType.INV_SATISFIABILITY, ctxt); + this.definition = statedef.invdef; StringBuilder sb = new StringBuilder(); sb.append("exists "); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInitObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInitObligation.java index 4d3374b50..06235616d 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInitObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInitObligation.java @@ -31,6 +31,7 @@ public class StateInitObligation extends ProofObligation public StateInitObligation(POStateDefinition def, POContextStack ctxt) { super(def.location, POType.STATE_INIT, ctxt); + this.definition = def.initdef; value = ctxt.getObligation("exists " + def.initPattern + " : " + def.name + " & " + def.initExpression); } } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/visitors/TCAnyValueGenerator.java b/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/visitors/TCAnyValueGenerator.java new file mode 100644 index 000000000..cf914ccbc --- /dev/null +++ b/vdmj/src/main/java/com/fujitsu/vdmj/tc/types/visitors/TCAnyValueGenerator.java @@ -0,0 +1,328 @@ +/******************************************************************************* + * + * 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 com.fujitsu.vdmj.tc.types.visitors; + +import com.fujitsu.vdmj.tc.types.TCBasicType; +import com.fujitsu.vdmj.tc.types.TCBooleanType; +import com.fujitsu.vdmj.tc.types.TCBracketType; +import com.fujitsu.vdmj.tc.types.TCCharacterType; +import com.fujitsu.vdmj.tc.types.TCClassType; +import com.fujitsu.vdmj.tc.types.TCField; +import com.fujitsu.vdmj.tc.types.TCFunctionType; +import com.fujitsu.vdmj.tc.types.TCInMapType; +import com.fujitsu.vdmj.tc.types.TCIntegerType; +import com.fujitsu.vdmj.tc.types.TCInvariantType; +import com.fujitsu.vdmj.tc.types.TCMapType; +import com.fujitsu.vdmj.tc.types.TCNamedType; +import com.fujitsu.vdmj.tc.types.TCNaturalOneType; +import com.fujitsu.vdmj.tc.types.TCNaturalType; +import com.fujitsu.vdmj.tc.types.TCOperationType; +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; +import com.fujitsu.vdmj.tc.types.TCRealType; +import com.fujitsu.vdmj.tc.types.TCRecordType; +import com.fujitsu.vdmj.tc.types.TCSeq1Type; +import com.fujitsu.vdmj.tc.types.TCSeqType; +import com.fujitsu.vdmj.tc.types.TCSet1Type; +import com.fujitsu.vdmj.tc.types.TCSetType; +import com.fujitsu.vdmj.tc.types.TCTokenType; +import com.fujitsu.vdmj.tc.types.TCType; +import com.fujitsu.vdmj.tc.types.TCUndefinedType; +import com.fujitsu.vdmj.tc.types.TCUnionType; +import com.fujitsu.vdmj.tc.types.TCUnknownType; +import com.fujitsu.vdmj.tc.types.TCUnresolvedType; +import com.fujitsu.vdmj.tc.types.TCVoidReturnType; +import com.fujitsu.vdmj.tc.types.TCVoidType; +import com.fujitsu.vdmj.values.BooleanValue; +import com.fujitsu.vdmj.values.CharacterValue; +import com.fujitsu.vdmj.values.IntegerValue; +import com.fujitsu.vdmj.values.MapValue; +import com.fujitsu.vdmj.values.NameValuePair; +import com.fujitsu.vdmj.values.NameValuePairList; +import com.fujitsu.vdmj.values.NaturalOneValue; +import com.fujitsu.vdmj.values.NaturalValue; +import com.fujitsu.vdmj.values.NilValue; +import com.fujitsu.vdmj.values.QuoteValue; +import com.fujitsu.vdmj.values.RationalValue; +import com.fujitsu.vdmj.values.RealValue; +import com.fujitsu.vdmj.values.RecordValue; +import com.fujitsu.vdmj.values.SeqValue; +import com.fujitsu.vdmj.values.SetValue; +import com.fujitsu.vdmj.values.TokenValue; +import com.fujitsu.vdmj.values.TupleValue; +import com.fujitsu.vdmj.values.UndefinedValue; +import com.fujitsu.vdmj.values.Value; +import com.fujitsu.vdmj.values.ValueList; +import com.fujitsu.vdmj.values.ValueSet; +import com.fujitsu.vdmj.values.VoidReturnValue; +import com.fujitsu.vdmj.values.VoidValue; + +public class TCAnyValueGenerator extends TCTypeVisitor +{ + @Override + public Value caseType(TCType node, Object arg) + { + throw new RuntimeException("Missing TCAnyValueGenerator method"); + } + + @Override + public Value caseBasicType(TCBasicType node, Object arg) + { + return caseType(node, arg); + } + + @Override + public Value caseBooleanType(TCBooleanType node, Object arg) + { + return new BooleanValue(true); + } + + @Override + public Value caseBracketType(TCBracketType node, Object arg) + { + return node.type.apply(this, arg); + } + + @Override + public Value caseCharacterType(TCCharacterType node, Object arg) + { + return new CharacterValue('a'); + } + + @Override + public Value caseClassType(TCClassType node, Object arg) + { + return null; // Can't do this? + } + + @Override + public Value caseFunctionType(TCFunctionType node, Object arg) + { + return null; // Can't do this? + } + + @Override + public Value caseInMapType(TCInMapType node, Object arg) + { + return new MapValue(); + } + + @Override + public Value caseIntegerType(TCIntegerType node, Object arg) + { + return caseNumericType(node, arg); + } + + @Override + public Value caseInvariantType(TCInvariantType node, Object arg) + { + return new IntegerValue(0); + } + + @Override + public Value caseMapType(TCMapType node, Object arg) + { + return new MapValue(); + } + + @Override + public Value caseNamedType(TCNamedType node, Object arg) + { + return node.type.apply(this, arg); + } + + @Override + public Value caseNaturalOneType(TCNaturalOneType node, Object arg) + { + try + { + return new NaturalOneValue(1); + } + catch (Exception e) + { + return null; // can't happen + } + } + + @Override + public Value caseNaturalType(TCNaturalType node, Object arg) + { + try + { + return new NaturalValue(1); + } + catch (Exception e) + { + return null; // can't happen + } + } + + @Override + public Value caseOperationType(TCOperationType node, Object arg) + { + return null; // Can't do this one? + } + + @Override + public Value caseOptionalType(TCOptionalType node, Object arg) + { + return new NilValue(); + } + + @Override + public Value caseParameterType(TCParameterType node, Object arg) + { + return null; // Can't do this one? + } + + @Override + public Value caseProductType(TCProductType node, Object arg) + { + ValueList list = new ValueList(); + + for (TCType type: node.types) + { + list.add(type.apply(this, arg)); + } + + return new TupleValue(list); + } + + @Override + public Value caseQuoteType(TCQuoteType node, Object arg) + { + return new QuoteValue(node.value); + } + + @Override + public Value caseRationalType(TCRationalType node, Object arg) + { + try + { + return new RationalValue(0.0); + } + catch (Exception e) + { + return null; // Can't happen + } + } + + @Override + public Value caseRealType(TCRealType node, Object arg) + { + try + { + return new RealValue(0.0); + } + catch (Exception e) + { + return null; // Can't happen + } + } + + @Override + public Value caseRecordType(TCRecordType node, Object arg) + { + NameValuePairList list = new NameValuePairList(); + + for (TCField field: node.fields) + { + list.add(new NameValuePair(field.tagname, field.type.apply(this, arg))); + } + + return new RecordValue(node, list); + } + + @Override + public Value caseSeq1Type(TCSeq1Type node, Object arg) + { + ValueList list = new ValueList(node.seqof.apply(this, arg)); + return new SeqValue(list); + } + + @Override + public Value caseSeqType(TCSeqType node, Object arg) + { + return new SeqValue(); + } + + @Override + public Value caseSet1Type(TCSet1Type node, Object arg) + { + ValueSet list = new ValueSet(node.setof.apply(this, arg)); + return new SetValue(list); + } + + @Override + public Value caseSetType(TCSetType node, Object arg) + { + return new SetValue(); + } + + @Override + public Value caseTokenType(TCTokenType node, Object arg) + { + return new TokenValue(node.argtypes.first().apply(this, arg)); + } + + @Override + public Value caseUndefinedType(TCUndefinedType node, Object arg) + { + return new UndefinedValue(); + } + + @Override + public Value caseUnionType(TCUnionType node, Object arg) + { + return node.types.first().apply(this, arg); // Just pick one + } + + @Override + public Value caseUnknownType(TCUnknownType node, Object arg) + { + return new UndefinedValue(); + } + + @Override + public Value caseUnresolvedType(TCUnresolvedType node, Object arg) + { + return new UndefinedValue(); // Should never happen + } + + @Override + public Value caseVoidReturnType(TCVoidReturnType node, Object arg) + { + return new VoidReturnValue(); + } + + @Override + public Value caseVoidType(TCVoidType node, Object arg) + { + return new VoidValue(); + } +}