From 04bf86cf5e49a43e2e704d965542b06d31906334 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Mon, 6 Nov 2023 09:50:52 +0000 Subject: [PATCH 1/6] QC add execCompleted test --- .../src/main/java/quickcheck/QuickCheck.java | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java index 3fddcf226..0fe85602d 100644 --- a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -442,6 +442,7 @@ else if (results.provedBy != null) IterableContext ictxt = addTypeParams(po, ctxt); Value execResult = new BooleanValue(false); ContextException exception = null; + boolean execCompleted = false; long before = System.currentTimeMillis(); try @@ -459,6 +460,8 @@ else if (results.provedBy != null) execResult = poexp.eval(ictxt); } while (ictxt.hasNext() && execResult.boolValue(ctxt)); + + execCompleted = true; } catch (ContextException e) { @@ -468,7 +471,8 @@ else if (results.provedBy != null) } else if (e.number == 4024) // 'not yet specified' expression reached { - execResult = new BooleanValue(true); // MAYBE, in effect + // MAYBE, in effect - execCompleted will be false + execResult = new BooleanValue(!po.kind.isExistential()); } else { @@ -515,7 +519,7 @@ else if (po.kind.isExistential()) { outcome = POStatus.PROVED; // An "exists" PO is PROVED, if true. } - else if (results.hasAllValues) + else if (results.hasAllValues && execCompleted) { outcome = POStatus.PROVED; // All values were tested and passed, so PROVED } @@ -569,8 +573,8 @@ else if (po.kind.isExistential()) // Principal exp is "exists..." } else { - String msg = String.format("Error: PO evaluation returns %s?\n", execResult.kind()); - infof("PO #%d, %s\n", po.number, msg); + String msg = String.format("Error: PO #%d evaluation returns %s?\n", po.number, execResult.kind()); + infoln(msg); po.setStatus(POStatus.FAILED); po.setCounterexample(null); po.setCounterMessage(msg); @@ -578,12 +582,13 @@ else if (po.kind.isExistential()) // Principal exp is "exists..." printBindings(bindings); infoln("----"); infoln(po); + errorCount++; } } catch (Exception e) { - String msg = String.format("Exception: %s", e.getMessage()); - infof("PO #%d, %s\n", po.number, msg); + String msg = String.format("Exception: PO #%d %s", po.number, e.getMessage()); + infoln(msg); po.setStatus(POStatus.FAILED); po.setCounterexample(null); po.setCounterMessage(msg); From 5cd78f60b587bc8d12a2cb2e9f9ca71cd9d8d9be Mon Sep 17 00:00:00 2001 From: nick_battle Date: Mon, 6 Nov 2023 09:55:50 +0000 Subject: [PATCH 2/6] Add provedBy "finite" when hasAllTypes succeeds --- examples/quickcheck/src/main/java/quickcheck/QuickCheck.java | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java index 0fe85602d..902b1e56b 100644 --- a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -510,6 +510,7 @@ else if (execResult instanceof BooleanValue) if (execResult.boolValue(ctxt)) { POStatus outcome = null; + String message = ""; if (didTimeout) { @@ -522,13 +523,15 @@ else if (po.kind.isExistential()) else if (results.hasAllValues && execCompleted) { outcome = POStatus.PROVED; // All values were tested and passed, so PROVED + message = " by finite types"; + po.setProvedBy("finite"); } else { outcome = POStatus.MAYBE; } - infof("PO #%d, %s %s\n", po.number, outcome.toString().toUpperCase(), duration(before, after)); + infof("PO #%d, %s%s %s\n", po.number, outcome.toString().toUpperCase(), message, duration(before, after)); po.setStatus(outcome); po.setCounterexample(null); po.setCounterMessage(null); From fea871562802d35c163c4d793772dcf2cfcb401e Mon Sep 17 00:00:00 2001 From: nick_battle Date: Mon, 6 Nov 2023 10:59:37 +0000 Subject: [PATCH 3/6] Add existential witness recording --- .../src/main/java/quickcheck/QuickCheck.java | 63 +++++++++++++++---- .../main/java/workspace/plugins/POPlugin.java | 5 ++ .../in/expressions/INExistsExpression.java | 22 +++++++ .../vdmj/in/patterns/INBindingSetter.java | 2 + .../vdmj/in/patterns/INMultipleTypeBind.java | 22 +++++++ .../fujitsu/vdmj/in/patterns/INTypeBind.java | 22 +++++++ .../java/com/fujitsu/vdmj/pog/POType.java | 2 +- .../com/fujitsu/vdmj/pog/ProofObligation.java | 6 ++ 8 files changed, 132 insertions(+), 12 deletions(-) diff --git a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java index 902b1e56b..e23efe6c8 100644 --- a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -519,6 +519,9 @@ else if (execResult instanceof BooleanValue) else if (po.kind.isExistential()) { outcome = POStatus.PROVED; // An "exists" PO is PROVED, if true. + Context path = getWitness(bindings); + String w = stringOfContext(path); + if (w != null) message = " witness " + w; } else if (results.hasAllValues && execCompleted) { @@ -556,7 +559,8 @@ else if (po.kind.isExistential()) // Principal exp is "exists..." { infof("PO #%d, FAILED %s: ", po.number, duration(before, after)); po.setStatus(POStatus.FAILED); - po.setCounterexample(printFailPath(bindings)); + printCounterexample(bindings); + po.setCounterexample(getCounterexample(bindings)); if (exception != null) { @@ -689,28 +693,63 @@ private void printBindings(List bindings) } } - private Context printFailPath(List bindings) + private Context getCounterexample(List bindings) { - Context path = null; + Context ctxt = null; for (INBindingSetter setter: bindings) { - path = setter.getCounterexample(); + ctxt = setter.getCounterexample(); - if (path != null) + if (ctxt != null) { break; // Any one will do - see INForAllExpression } } + + return ctxt; + } + + private Context getWitness(List bindings) + { + Context ctxt = null; + for (INBindingSetter setter: bindings) + { + ctxt = setter.getWitness(); + + if (ctxt != null) + { + break; // Any one will do - see INExistsExpression + } + } + + return ctxt; + } + + private void printCounterexample(List bindings) + { + Context path = getCounterexample(bindings); + String cex = stringOfContext(path); + + if (cex == null) + { + infoln("No counterexample"); + } + else + { + infoln("Counterexample: " + cex); + } + } + + private String stringOfContext(Context path) + { if (path == null || path.isEmpty()) { - infof("No counterexample\n"); - printBindings(bindings); return null; } - infof("Counterexample: "); + StringBuilder result = new StringBuilder(); String sep = ""; Context ctxt = path; @@ -718,15 +757,17 @@ private Context printFailPath(List bindings) { for (TCNameToken name: ctxt.keySet()) { - infof("%s%s = %s", sep, name, ctxt.get(name)); + result.append(sep); + result.append(name); + result.append(" = "); + result.append(ctxt.get(name)); sep = ", "; } ctxt = ctxt.outer; } - infoln(""); - return path; + return result.toString(); } private String duration(long time) diff --git a/lsp/src/main/java/workspace/plugins/POPlugin.java b/lsp/src/main/java/workspace/plugins/POPlugin.java index 9dc513942..d68d55f01 100644 --- a/lsp/src/main/java/workspace/plugins/POPlugin.java +++ b/lsp/src/main/java/workspace/plugins/POPlugin.java @@ -233,6 +233,11 @@ else if (file.isDirectory()) messages.add(new VDMWarning(9001, po.countermessage, po.location)); } + if (po.witness != null) + { + json.put("witness", "PO #" + po.number + ": " + po.witness); + } + poList.add(json); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INExistsExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INExistsExpression.java index 08829dd47..6dce6eb75 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INExistsExpression.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INExistsExpression.java @@ -109,6 +109,7 @@ public Value eval(Context ctxt) { if (!v.equals(nvp.value)) { + setWitness(evalContext); matches = false; break; // This quantifier set does not match } @@ -119,6 +120,7 @@ public Value eval(Context ctxt) { if (matches && predicate.eval(evalContext).boolValue(ctxt)) { + setWitness(evalContext); return new BooleanValue(true); } } @@ -177,6 +179,26 @@ private void setCounterexample(Context ctxt, boolean didTimeout) } } } + + /** + * This is used by the QuickCheck plugin to report which values succeeded. + */ + private void setWitness(Context ctxt) + { + for (INMultipleBind bind: bindList) + { + if (bind instanceof INBindingSetter) // Type and multitype binds + { + INBindingSetter setter = (INBindingSetter)bind; + + if (setter.getBindValues() != null) // One we care about (set QC values for) + { + setter.setWitness(ctxt); + break; // Just one will do - see QC printFailPath + } + } + } + } @Override public R apply(INExpressionVisitor visitor, S arg) diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INBindingSetter.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INBindingSetter.java index 910f01a08..6adbc0b02 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INBindingSetter.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INBindingSetter.java @@ -37,4 +37,6 @@ public interface INBindingSetter public TCType getType(); public void setCounterexample(Context ctxt, boolean didTimeout); public Context getCounterexample(); + public void setWitness(Context ctxt); + public Context getWitness(); } diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INMultipleTypeBind.java b/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INMultipleTypeBind.java index 90b0bc6d0..614a37676 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INMultipleTypeBind.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/in/patterns/INMultipleTypeBind.java @@ -44,6 +44,7 @@ public class INMultipleTypeBind extends INMultipleBind implements INBindingSette private ValueList bindValues = null; private Context bindCounterexample = null; + private Context bindWitness = null; private boolean bindPermuted = false; private boolean bindOverride = false; private long bindTimeout = 0; @@ -80,6 +81,8 @@ public void setBindValues(ValueList values, long timeout) } didTimeout = false; + bindCounterexample = null; + bindWitness = null; } @Override @@ -121,6 +124,25 @@ public Context getCounterexample() return bindCounterexample; } + @Override + public void setWitness(Context ctxt) + { + if (ctxt == null) + { + bindWitness = null; + } + else if (bindWitness == null) // Catch first witness, don't overwrite + { + bindWitness = ctxt; + } + } + + @Override + public Context getWitness() + { + return bindWitness; + } + @Override public TCType getType() { 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 424571c5f..b21243a0c 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 @@ -44,6 +44,7 @@ public class INTypeBind extends INBind implements INBindingSetter private ValueList bindValues = null; private Context bindCounterexample = null; + private Context bindWitness = null; private boolean bindPermuted = false; private boolean bindOverride = false; private long bindTimeout = 0; @@ -74,6 +75,8 @@ public void setBindValues(ValueList values, long timeout) } didTimeout = false; + bindCounterexample = null; + bindWitness = null; } @Override @@ -120,6 +123,25 @@ public Context getCounterexample() { return bindCounterexample; } + + @Override + public void setWitness(Context ctxt) + { + if (ctxt == null) + { + bindWitness = null; + } + else if (bindWitness == null) // Catch first witness, don't overwrite + { + bindWitness = ctxt; + } + } + + @Override + public Context getWitness() + { + return bindWitness; + } @Override public INMultipleBindList getMultipleBindList() diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POType.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POType.java index f0f8ac994..df1d99ed2 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POType.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POType.java @@ -33,7 +33,7 @@ public enum POType FUNC_SATISFIABILITY("function satisfiability", true), FUNC_PATTERNS("function parameter patterns", true), LET_BE_EXISTS("let be st existence", true), - UNIQUE_EXISTENCE("unique existence binding", true), + UNIQUE_EXISTENCE("unique existence binding"), // Note: not existential! FUNC_ITERATION("function iteration"), MAP_ITERATION("map iteration"), FUNC_COMPOSE("function compose"), 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 e4e935a6e..3e7ed83bc 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java @@ -47,6 +47,7 @@ abstract public class ProofObligation implements Comparable public Context counterexample; public String countermessage; public String provedBy; + public String witness; private int var = 1; private TCExpression checkedExpression = null; @@ -104,6 +105,11 @@ public void setCounterMessage(String message) { this.countermessage = message; } + + public void setWitness(String witness) + { + this.witness = witness; + } @Override public String toString() From 9c7dcbb325bf39b3c740602c1f072f07f010f862 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Mon, 6 Nov 2023 12:14:58 +0000 Subject: [PATCH 4/6] Revise isExistential to use context stack as well --- .../src/main/java/quickcheck/QuickCheck.java | 6 ++--- .../com/fujitsu/vdmj/pog/POCaseContext.java | 6 +++++ .../java/com/fujitsu/vdmj/pog/POContext.java | 5 ++++ .../com/fujitsu/vdmj/pog/POContextStack.java | 26 +++++++++++++++++++ .../java/com/fujitsu/vdmj/pog/POType.java | 2 +- .../com/fujitsu/vdmj/pog/ProofObligation.java | 8 ++++++ 6 files changed, 49 insertions(+), 4 deletions(-) diff --git a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java index e23efe6c8..28fd65c7a 100644 --- a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -472,7 +472,7 @@ else if (results.provedBy != null) else if (e.number == 4024) // 'not yet specified' expression reached { // MAYBE, in effect - execCompleted will be false - execResult = new BooleanValue(!po.kind.isExistential()); + execResult = new BooleanValue(!po.isExistential()); } else { @@ -516,7 +516,7 @@ else if (execResult instanceof BooleanValue) { outcome = POStatus.TIMEOUT; } - else if (po.kind.isExistential()) + else if (po.isExistential()) { outcome = POStatus.PROVED; // An "exists" PO is PROVED, if true. Context path = getWitness(bindings); @@ -548,7 +548,7 @@ else if (results.hasAllValues && execCompleted) po.setCounterexample(null); po.setCounterMessage(null); } - else if (po.kind.isExistential()) // Principal exp is "exists..." + else if (po.isExistential()) // Principal exp is "exists..." { infof("PO #%d, MAYBE %s\n", po.number, duration(before, after)); po.setStatus(POStatus.MAYBE); diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POCaseContext.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POCaseContext.java index 5850434b2..fc5c38ac5 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POCaseContext.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POCaseContext.java @@ -41,6 +41,12 @@ public POCaseContext(POPattern pattern, TCType type, POExpression exp) this.type = type; this.exp = exp; } + + @Override + public boolean isExistential() + { + return !pattern.isSimple(); + } @Override public String getContext() 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 c3a2b7efe..81e5ddc26 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContext.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContext.java @@ -50,6 +50,11 @@ public POAnnotationList getAnnotations() { return null; } + + public boolean isExistential() + { + return false; + } public TCTypeList getTypeParams() { 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 a3f64cbf8..0b6772dcd 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POContextStack.java @@ -119,6 +119,32 @@ public POAnnotationList getAnnotations() return null; } + + public boolean isExistential() + { + for (POContext ctxt: this) + { + if (!(ctxt instanceof PONameContext)) + { + return ctxt.isExistential(); + } + } + + return false; + } + + public boolean hasNone() + { + for (POContext ctxt: this) + { + if (!(ctxt instanceof PONameContext)) + { + return false; // Has something significant + } + } + + return true; + } public TCTypeList getTypeParams() { diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POType.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POType.java index df1d99ed2..7a7bfab80 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/POType.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/POType.java @@ -49,7 +49,7 @@ public enum POType SEQ_MODIFICATION("sequence modification"), VALUE_BINDING("value binding", true), SUB_TYPE("subtype"), - CASES_EXHAUSTIVE("cases exhaustive", true), + CASES_EXHAUSTIVE("cases exhaustive"), INVARIANT("type invariant"), RECURSIVE("recursive function"), STATE_INVARIANT("state invariant"), 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 3e7ed83bc..22036c52e 100644 --- a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java +++ b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java @@ -51,6 +51,7 @@ abstract public class ProofObligation implements Comparable private int var = 1; private TCExpression checkedExpression = null; + private boolean existential = false; public ProofObligation(LexLocation location, POType kind, POContextStack ctxt) { @@ -70,6 +71,8 @@ public ProofObligation(LexLocation location, POType kind, POContextStack ctxt) { this.status = POStatus.UNCHECKED; // Implies unproved } + + existential = ctxt.isExistential() || (ctxt.hasNone() && kind.isExistential()); POGetMatchingExpressionVisitor.init(); // Reset the "any" count, before PO creation } @@ -110,6 +113,11 @@ public void setWitness(String witness) { this.witness = witness; } + + public boolean isExistential() + { + return existential; + } @Override public String toString() From 92c2368f78a968e98ca748b081051d8f99832ba5 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Mon, 6 Nov 2023 12:18:20 +0000 Subject: [PATCH 5/6] Set PO witness value --- examples/quickcheck/src/main/java/quickcheck/QuickCheck.java | 1 + 1 file changed, 1 insertion(+) diff --git a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java index 28fd65c7a..511ade32e 100644 --- a/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java +++ b/examples/quickcheck/src/main/java/quickcheck/QuickCheck.java @@ -521,6 +521,7 @@ else if (po.isExistential()) outcome = POStatus.PROVED; // An "exists" PO is PROVED, if true. Context path = getWitness(bindings); String w = stringOfContext(path); + po.setWitness(w); if (w != null) message = " witness " + w; } else if (results.hasAllValues && execCompleted) From c9fa03130d5f7a9fb6718413a3038508bae5e9e8 Mon Sep 17 00:00:00 2001 From: nick_battle Date: Mon, 6 Nov 2023 14:34:26 +0000 Subject: [PATCH 6/6] Update VDMUtil source for PP and RT, and untweak Java --- stdlib/src/main/java/VDMUtil.java | 6 +++--- stdlib/src/main/resources/VDMUtil.vdmpp | 8 ++++++-- stdlib/src/main/resources/VDMUtil.vdmrt | 8 ++++++-- 3 files changed, 15 insertions(+), 7 deletions(-) diff --git a/stdlib/src/main/java/VDMUtil.java b/stdlib/src/main/java/VDMUtil.java index ce981af2a..31c5a9797 100644 --- a/stdlib/src/main/java/VDMUtil.java +++ b/stdlib/src/main/java/VDMUtil.java @@ -68,7 +68,7 @@ public static Value val2seq_of_char(Value arg) } @VDMFunction - public static Value seq_of_char2val(Value arg) + public static Value seq_of_char2val_(Value arg) // Note, with underscore - see VDM { ValueList result = new ValueList(); @@ -93,7 +93,7 @@ public static Value seq_of_char2val(Value arg) INExpression inexp = ClassMapper.getInstance(INNode.MAPPINGS).convert(tcexp); result.add(new BooleanValue(true)); - Context ctxt = new Context(null, "seq_of_char2val", null); + Context ctxt = new Context(null, "seq_of_char2val_", null); ctxt.setThreadState(null); result.add(inexp.eval(ctxt)); } @@ -123,7 +123,7 @@ public static Value classname(Value arg) } } - public Value get_file_pos(Context ctxt) + public static Value get_file_pos(Context ctxt) { try { diff --git a/stdlib/src/main/resources/VDMUtil.vdmpp b/stdlib/src/main/resources/VDMUtil.vdmpp index af6c09642..b53ccc8f3 100644 --- a/stdlib/src/main/resources/VDMUtil.vdmpp +++ b/stdlib/src/main/resources/VDMUtil.vdmpp @@ -29,8 +29,12 @@ val2seq_of_char(x) == is not yet specified; -- RESULT.#1 = false implies a conversion failure static public seq_of_char2val[@p]:seq1 of char -> bool * [@p] seq_of_char2val(s) == - is not yet specified - post let mk_(b,t) = RESULT in not b => t = nil; +let mk_(b, v) = seq_of_char2val_(s) in + if is_(v, @p) then mk_(b, v) else mk_(false, nil) +post let mk_(b,t) = RESULT in not b => t = nil; + +static seq_of_char2val_:seq1 of char -> bool * ? +seq_of_char2val_(s) == is not yet specified static public classname[@T] : @T -> [seq1 of char] classname(s) == is not yet specified; diff --git a/stdlib/src/main/resources/VDMUtil.vdmrt b/stdlib/src/main/resources/VDMUtil.vdmrt index af6c09642..b53ccc8f3 100644 --- a/stdlib/src/main/resources/VDMUtil.vdmrt +++ b/stdlib/src/main/resources/VDMUtil.vdmrt @@ -29,8 +29,12 @@ val2seq_of_char(x) == is not yet specified; -- RESULT.#1 = false implies a conversion failure static public seq_of_char2val[@p]:seq1 of char -> bool * [@p] seq_of_char2val(s) == - is not yet specified - post let mk_(b,t) = RESULT in not b => t = nil; +let mk_(b, v) = seq_of_char2val_(s) in + if is_(v, @p) then mk_(b, v) else mk_(false, nil) +post let mk_(b,t) = RESULT in not b => t = nil; + +static seq_of_char2val_:seq1 of char -> bool * ? +seq_of_char2val_(s) == is not yet specified static public classname[@T] : @T -> [seq1 of char] classname(s) == is not yet specified;