Overture Tool
Formal Modelling in VDM
VCParser-masterSL
Author: Tomohiro Oda
This example is created by Tomohiro Oda and it illustrates how it is possible to use higher-order functions in VDM-SL to create parser elements that can be put together in a compositional fashion. This model can be used as a kind of library that one can play with manipulating strings into a VDM AST representation.
| Properties | Values |
|---|---|
| Language Version: | vdm10 |
| Entry point : | MMParser`eval(“1+1+4+0”) |
MMParser.vdmsl
module MMParser
/***
MMParser
Author: Tomohiro Oda
Version: 0.01
License: the MIT License
Copyright (c) 2013 Tomohiro Oda and Software Research Associates, Inc.
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in
all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
THE SOFTWARE.
***/
imports from VCParser all
exports functions eval : seq of char -> [int];
definitions
types
TREE = VCParser`TREE;
values
series = VCParser`series;
either = VCParser`either;
star = VCParser`star;
trimBlanks = VCParser`trimBlanks;
integer = VCParser`integer;
takeChar = VCParser`takeChar;
transtree = VCParser`transtree;
parseInt = trimBlanks(integer);
parseMul = series([takeChar('*'), parseInt]);
parseDiv = series([takeChar('/'), parseInt]);
parseTerm =
transtree(
liftOperator, series([parseInt, star(either([parseMul, parseDiv]))]));
parseAdd = series([takeChar('+'), parseTerm]);
parseSub = series([takeChar('-'), parseTerm]);
parseExpression =
transtree(
liftOperator, series([parseTerm, star(either([parseAdd, parseSub]))]));
functions
liftOperator : VCParser`TREE -> VCParser`TREE
liftOperator(tree) ==
let mk_VCParser`TREE(-, [left, right]) = tree
in
let mk_VCParser`TREE(-, rights) = right
in
cases rights:
[] -> left,
[mk_VCParser`TREE(-, [mk_VCParser`TREE(-, operator), operand])] ^ rest ->
liftOperator(
mk_VCParser`TREE(
nil,
[mk_VCParser`TREE(operator, [left, operand]),
mk_VCParser`TREE(nil, rest)]))
end;
evalInt : seq of char -> int
evalInt(string) ==
cases string:
"-" ^ rest -> evalInt(rest) * -1,
[] -> 0,
others ->
evalInt([string(i) | i in set {1, ..., len string - 1}]) * 10
+ {'0' |-> 0, '1' |-> 1, '2' |-> 2, '3' |-> 3, '4' |-> 4, '5' |-> 5,
'6' |-> 6, '7' |-> 7, '8' |-> 8, '9' |-> 9}(
string(len string))
end
measure lenChar;
lenChar : seq of char -> nat
lenChar(x) == len x;
evalTree : TREE -> int
evalTree(tree) ==
cases tree:
mk_VCParser`TREE("int", contents) -> evalInt(contents),
mk_VCParser`TREE(nil, contents) -> evalInt(contents),
mk_VCParser`TREE("*", [e1, e2]) -> evalTree(e1) * evalTree(e2),
mk_VCParser`TREE("/", [e1, e2]) -> evalTree(e1) div evalTree(e2),
mk_VCParser`TREE("+", [e1, e2]) -> evalTree(e1) + evalTree(e2),
mk_VCParser`TREE("-", [e1, e2]) -> evalTree(e1) - evalTree(e2)
end;
hasDivZero : VCParser`TREE -> bool
hasDivZero(tree) == cases tree:
mk_VCParser`TREE("/", [-, mk_VCParser`TREE("int", "0")]) -> true,
mk_VCParser`TREE("/", [-, mk_VCParser`TREE("int", "-0")]) -> true,
mk_VCParser`TREE("int", -),
mk_VCParser`TREE(nil, -) -> false,
mk_VCParser`TREE(-, [tree1, tree2]) -> hasDivZero(tree1) or hasDivZero(tree2)
end;
eval : seq of char -> [int]
eval(string) ==
cases parseExpression(string):
mk_VCParser`PARSED(tree, []) -> if hasDivZero(tree) then nil else evalTree(tree),
others -> nil
end;
end MMParser
MMParserTest.vdmsl
module MMParserTest
/***
Combinatorial Testing Module for MMParser.
requires vdm10 turned on.
***/
imports
from MMParser functions eval renamed eval;
exports all
definitions
traces
integer:
let s in set {"", "-"} in
let d1 in set {"1", "2", "3", "4", "5", "6", "7", "8", "9"} in
let d2 in set {"0", "1", "2", "3", "4", "5", "6", "7", "8", "9"} in
eval(s^d1^d2);
two_terms:
let s1, s2 in set {"", "-"} in
let n1, n2 in set {"39", "441", "0"} in
let op1 in set {"*", "/", "+", "-"} in
eval(s1 ^ n1 ^ op1 ^ s2 ^ n2);
three_terms:
let s1, s2, s3 in set {"", "-"} in
let n1, n2, n3 in set {"39", "441", "0"} in
let op1, op2 in set {"*", "/", "+", "-"} in
eval(s1 ^ n1 ^ op1 ^ s2 ^ n2 ^ op2 ^ s3 ^ n3);
four_terms:
let i1, i2, i3, i4 in set {"-39", "441", "0"} in
let op1, op2, op3 in set {"*", "/", "+", "-"} in
eval(i1 ^ op1 ^ i2 ^ op2 ^ i3 ^ op3 ^ i4);
end MMParserTest
VCParserSupp.vdmsl
module VCParserSupp
/***
VCParserSupp
Author: Tomohiro Oda and Paul Chisholm
Version: 0.01
License: the MIT License
Copyright (c) 2016 Tomohiro Oda, Paul Chisholm
and Software Research Associates, Inc.
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in
all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
THE SOFTWARE.
****************************************************************************
This module supplements the VCParser module with additional convenience functions.
Note this module depends on modules Char, Numeric and Seq that are in the ISO8601 example located at
http://overturetool.org/download/examples/VDMSL/
***/
imports from VCParser values
digit renamed digit
lowerAlphabet renamed lowerAlphabet
upperAlphabet renamed upperAlphabet
alphabet renamed alphabet
types PARSER renamed PARSER
SOURCE renamed SOURCE
PARSED renamed PARSED
TREE renamed TREE
ERROR renamed ERROR
LABEL renamed LABEL
functions label renamed label
either renamed either
concat renamed concat
iterate renamed iterate
takeChar renamed takeChar,
from Seq all,
from Numeric all,
from Char all
exports values lowerAlphanum, upperAlphanum, alphanum, octal, hex: PARSER
functions takeNumeric : [nat1] * [nat1] -> PARSER
takeFixedNumeric : nat1 -> PARSER
takeBoundedString: seq1 of char * PARSER * nat * nat -> PARSER
takeUpto : seq1 of char * [PARSER] +> PARSER
takeUptoOneOf : seq of seq1 of char * [seq1 of char] * [PARSER] +> PARSER
getContent : LABEL * TREE +> seq of char
getContentNat : LABEL * TREE +> nat
getTrees : LABEL * TREE +> seq of TREE
getTree : LABEL * TREE +> TREE
isEmpty : TREE +> bool
prune : PARSED -> PARSED
pruneTree : TREE -> TREE
format : PARSED -> seq of char
formatTree : TREE * nat -> seq of char
definitions
values
TABSIZE = 2;
-- Recognise a lower case alphanumeric character.
lowerAlphanum =
label("lowerAlphanum", either([lowerAlphabet, digit]));
-- Recognise an upper case alphanumeric character.
upperAlphanum =
label("upperAlphanum", either([upperAlphabet, digit]));
-- Recognise an alphanumeric character.
alphanum =
label("alphabet", either([alphabet, digit]));
-- Recognise an octal digit.
octal =
label(
"octal",
either([takeChar("01234567"(index)) | index in set {1, ..., 8}]));
-- Recognise a hexadecimal digit.
hex =
label(
"hex",
either([takeChar("0123456789ABCDEFabcdef"(index)) | index in set {1, ..., 22}]));
functions
-- Recognise a numeric value optionally specifying the minimum and maximum digits.
takeNumeric: [nat1] * [nat1] -> PARSER
takeNumeric(m, n) == let m1 = if m = nil then 1 else m
in concat(iterate(digit, m1, n))
pre m <> nil and n <> nil => m <= n;
-- Recognise a fixed length numeric value.
takeFixedNumeric: nat1 -> PARSER
takeFixedNumeric(n) == takeNumeric(n, n);
-- Recognise a string optionally specifying a minimum and maximum length.
-- While the parser argument can be arbitrary, the intent is it recognises a single character.
takeBoundedString: seq1 of char * PARSER * nat * nat -> PARSER
takeBoundedString(lbl, parser, min, max) == label(lbl, concat(iterate(parser, min, max)))
pre min <= max;
-- Recognise characters in the source till a specified token is reached.
-- If an optional parser is specified, use it to parse the recognised string.
takeUpto: seq1 of char * [PARSER] +> PARSER
takeUpto(word, parser) ==
lambda source : SOURCE &
cases Seq`indexOfSeqOpt[char](word, source):
nil -> mk_PARSED(mk_ERROR(word ^ " not found"), source),
index -> let recognised = [ source(i) | i in set {1,...,index-1} ],
remainder = [ source(i) | i in set {index,...,len source} ] in
if parser = nil
then mk_PARSED(mk_TREE(nil, recognised), remainder)
else let mk_PARSED(tree, rest) = parser(recognised) in
cases tree:
mk_ERROR(-) -> mk_PARSED(mk_ERROR("unrecognised"), source),
mk_TREE(-,-) -> if Char`isWhiteSpaces(rest)
then mk_PARSED(tree, remainder)
else mk_PARSED(mk_ERROR("excess"), rest^remainder)
end
end;
-- Recognise characters in the source till one of a specified sequence of tokens is reached.
-- If no such token is found, and an optional terminator is provided, recognise characters up to the terminator.
-- If a sequence is recognised and an optional parser is specified, use it to parse the recognised string.
takeUptoOneOf: seq of seq1 of char * [seq1 of char] * [PARSER] +> PARSER
takeUptoOneOf(tokens, term, parser) ==
lambda source : SOURCE &
cases tokens:
[] -> if term = nil
then mk_PARSED(mk_ERROR("not found"), source)
else takeUpto(term, parser)(source),
[tok]^rest -> let mk_PARSED(tree, source1) = takeUpto(tok, parser)(source) in
cases tree:
mk_ERROR(-) -> takeUptoOneOf(rest, term, parser)(source),
mk_TREE(-,-) -> mk_PARSED(tree, source1)
end
end;
/*
Convenience functions for extracting items from a parse tree.
*/
-- Get the character content.
getContent: LABEL * TREE +> seq of char
getContent(lbl, mk_TREE(tlabel,content)) == content
pre (lbl = nil or lbl = tlabel) and is_(content, seq of char);
-- Get the character content as a natural number.
getContentNat: LABEL * TREE +> nat
getContentNat(lbl, tree) == Numeric`decodeNat(getContent(lbl,tree))
pre pre_getContent(lbl, tree) and Char`isDigits(tree.contents);
-- Get the sequence of sub trees.
getTrees: LABEL * TREE +> seq of TREE
getTrees(lbl, mk_TREE(tlabel,content)) == content
pre (lbl = nil or lbl = tlabel) and is_(content, seq of TREE);
-- Get the only sub tree.
getTree: LABEL * TREE +> TREE
getTree(lbl, tree) == tree.contents(1)
pre pre_getTrees(lbl, tree) and len tree.contents = 1;
-- Is a tree empty (has not label or content)?
isEmpty : TREE +> bool
isEmpty(mk_TREE(tlabel,content)) == tlabel = nil and content = [];
/*
Convenience functions for flattening out parse trees:
- remove empty sub trees;
- lift sub components up where a nil label is encountered.
*/
-- Filter out empty subtrees from a parse result.
prune : PARSED -> PARSED
prune(mk_PARSED(parsed, remaining)) ==
if
is_ERROR(parsed)
then
mk_PARSED(parsed, remaining)
else
mk_PARSED(pruneTree(liftTree(parsed)), remaining);
-- Filter out empty subtrees from a tree.
pruneTree : TREE -> TREE
pruneTree(mk_TREE(lbl, contents)) ==
if
is_(contents, seq of char)
then
mk_TREE(lbl, contents)
else
mk_TREE(lbl, pruneTrees(contents));
-- Prune a sequence of trees.
pruneTrees : seq of TREE -> seq of TREE
pruneTrees(trees) == [ pruneTree(trees(i)) | i in set inds trees & not isEmpty(pruneTree(trees(i))) ];
-- Lift subtrees with a nil label up a level.
liftTree : TREE -> TREE
liftTree(mk_TREE(lbl,contents)) ==
if is_(contents, seq of char)
then mk_TREE(lbl,contents)
else let lifted = liftTrees(contents)
in if lbl = nil and len lifted = 1
then lifted(1)
else mk_TREE(lbl,lifted);
-- Lift a sequence of subtrees.
liftTrees : seq of TREE -> seq of TREE
liftTrees(trees) == conc [ liftTreeSeq(trees(i)) | i in set inds trees ];
-- Auxiliary function for lifting subtrees.
-- Produces a sequence of trees in case the top level tree has a nil label.
liftTreeSeq : TREE -> seq of TREE
liftTreeSeq(mk_TREE(lbl,contents)) ==
if is_(contents, seq of char)
then [mk_TREE(lbl,contents)]
else let lifted = liftTrees(contents)
in if lbl = nil
then lifted
else [mk_TREE(lbl,lifted)];
/*
Convenience functions for creating a pretty printed text version of a parse tree.
*/
-- Format a parse result as text.
format : PARSED -> seq of char
format(mk_PARSED(parsed, remaining)) ==
formatTreeOrError(parsed) ^ "Remaining: [" ^ remaining ^ "]";
-- Format a parse tree or parse error as text.
formatTreeOrError : TREE| ERROR -> seq of char
formatTreeOrError(treeOrError) ==
if
is_ERROR(treeOrError)
then
"Error: " ^ treeOrError.message ^ "\n"
else
"Parse Tree:\n" ^ formatTree(treeOrError, TABSIZE);
-- Format a parse tree as text.
formatTree : TREE * nat -> seq of char
formatTree(mk_TREE(lbl, contents), n) ==
let lblstr = if lbl = nil then "" else lbl
in indent(n) ^ "'" ^ lblstr ^ "'\n" ^ formatContent(contents, n + TABSIZE);
-- Format as text the parse tree content (text or sequence of subtrees).
formatContent : (seq of TREE | seq of char) * nat -> seq of char
formatContent(tt, n) ==
if
is_(tt, seq of char)
then
indent(n) ^ "[" ^ tt ^ "]\n"
else
conc [formatTree(tt(i), n) | i in set inds tt];
-- Create a sequence of spaces.
indent : nat +> seq of char
indent(n) == [' ' | i in set {1, ..., n}];
end VCParserSupp
Seq.vdmsl
/*
A module that specifies and defines general purpose functions over sequences.
All functions are explicit and executable. Where a non-executable condition adds value, it
is included as a comment.
*/
module Seq
imports from Numeric all
exports functions sum: seq of real +> real
prod: seq of real +> real
min: seq1 of real +> real
max: seq1 of real +> real
inSeq[@a]: @a * seq of @a +> bool
indexOf[@a]: @a * seq1 of @a +> nat1
indexOfSeq[@a]: seq1 of @a * seq1 of @a +> nat1
indexOfSeqOpt[@a]: seq1 of @a * seq1 of @a +> [nat1]
numOccurs[@a]: @a * seq of @a +> nat
permutation[@a]: seq of @a * seq of @a +> bool
preSeq[@a]: seq of @a * seq of @a +> bool
postSeq[@a]: seq of @a * seq of @a +> bool
subSeq[@a]: seq of @a * seq of @a +> bool
replicate[@a]: nat * @a +> seq of @a
padLeft[@a]: seq of @a * @a * nat +> seq of @a
padRight[@a]: seq of @a * @a * nat +> seq of @a
padCentre[@a]: seq of @a * @a * nat +> seq of @a
dropWhile[@a]: (@a +> bool) * seq of @a +> seq of @a
xform[@a,@b]: (@a +> @b) * seq of @a +> seq of @b
fold[@a]: (@a * @a +> @a) * @a * seq of @a +> @a
fold1[@a]: (@a * @a +> @a) * seq1 of @a +> @a
zip[@a,@b]: seq of @a * seq of @b +> seq of (@a * @b)
unzip[@a,@b]: seq of (@a * @b) +> seq of @a * seq of @b
isDistinct[@a]: seq of @a +> bool
app[@a]: seq of @a * seq of @a +> seq of @a
setOf[@a]: seq of @a +> set of @a
format[@a]: (@a +> seq of char) * seq of char * seq of @a +> seq of char
definitions
functions
-- The sum of a sequence of numerics.
sum: seq of real +> real
sum(s) == fold[real](Numeric`add,0,s);
-- The product of a sequence of numerics.
prod: seq of real +> real
prod(s) == fold[real](Numeric`mult,1,s);
-- The minimum of a sequence of numerics.
min: seq1 of real +> real
min(s) == fold1[real](Numeric`min,s)
post RESULT in set elems s and forall e in set elems s & RESULT <= e;
-- The maximum of a sequence of numerics.
max: seq1 of real +> real
max(s) == fold1[real](Numeric`max,s)
post RESULT in set elems s and forall e in set elems s & RESULT >= e;
-- Does an element appear in a sequence?
inSeq[@a]: @a * seq of @a +> bool
inSeq(e,s) == e in set elems s;
-- The position an item appears in a sequence?
indexOf[@a]: @a * seq1 of @a +> nat1
indexOf(e,s) == cases s:
[-] -> 1,
[f]^ss -> if e=f then 1 else 1 + indexOf[@a](e,ss)
end
pre inSeq[@a](e,s)
measure size0;
-- The position a subsequence appears in a sequence.
indexOfSeq[@a]: seq1 of @a * seq1 of @a +> nat1
indexOfSeq(r,s) == if preSeq[@a](r,s)
then 1
else 1 + indexOfSeq[@a](r, tl s)
pre subSeq[@a](r,s)
measure size3;
-- The position a subsequence appears in a sequence?
indexOfSeqOpt[@a]: seq1 of @a * seq1 of @a +> [nat1]
indexOfSeqOpt(r,s) == if subSeq[@a](r,s) then indexOfSeq[@a](r, s) else nil;
-- The number of times an element appears in a sequence.
numOccurs[@a]: @a * seq of @a +> nat
numOccurs(e,sq) == len [ 0 | i in seq sq & i = e ];
-- Is one sequence a permutation of another?
permutation[@a]: seq of @a * seq of @a +> bool
permutation(sq1,sq2) ==
len sq1 = len sq2 and
forall x in seq sq1 & numOccurs[@a](x,sq1) = numOccurs[@a](x,sq2);
-- Is one sequence a prefix of another?
preSeq[@a]: seq of @a * seq of @a +> bool
preSeq(pres,full) == pres = full(1,...,len pres);
-- Is one sequence a suffix of another?
postSeq[@a]: seq of @a * seq of @a +> bool
postSeq(posts,full) == preSeq[@a](reverse posts, reverse full);
-- Is one sequence a subsequence of another sequence?
subSeq[@a]: seq of @a * seq of @a +> bool
subSeq(sub,full) == sub = [] or (exists i,j in set inds full & sub = full(i,...,j));
-- Create a sequence of identical elements.
replicate[@a]: nat * @a +> seq of @a
replicate(n,x) == [ x | i in set {1,...,n} ]
post len RESULT = n and forall y in seq RESULT & y = x;
-- Pad a sequence on the left with a given item up to a specified length.
padLeft[@a]: seq of @a * @a * nat +> seq of @a
padLeft(sq,x,n) == replicate[@a](n-len sq, x) ^ sq
pre n >= len sq
post len RESULT = n and postSeq[@a](sq, RESULT);
-- Pad a sequence on the right with a given item up to a specified length.
padRight[@a]: seq of @a * @a * nat +> seq of @a
padRight(sq,x,n) == sq ^ replicate[@a](n-len sq, x)
pre n >= len sq
post len RESULT = n and preSeq[@a](sq, RESULT);
-- Pad a sequence with a given item such that it is centred in a specified length.
-- If padded by an odd number, add the extra item on the right.
padCentre[@a]: seq of @a * @a * nat +> seq of @a
padCentre(sq,x,n) == let space = if n <= len sq then 0 else n - len sq
in padRight[@a](padLeft[@a](sq,x,len sq + (space div 2)),x,n);
-- trim[@a]: seq of @a * (@a +> bool) +> seq of @a
-- trim(s, p) == trimpre(reverse(trimpre(reverse s, p)), p);
-- post exists s1,s2: seq of char & s = s1 ^ RESULT ^ s2 and isDigits(s1) and isDigits(s2);
-- Drop items from a sequence while a predicate is true.
dropWhile[@a]: (@a +> bool) * seq of @a +> seq of @a
dropWhile(p, s) == cases s:
[] -> [],
[x] ^ t -> if p(x) then dropWhile[@a](p, t) else s
end
post postSeq[@a](RESULT, s) and
(RESULT = [] or not p(RESULT(1))) and
forall i in set {1,...,(len s - len RESULT)} & p(s(i))
measure size5;
-- Apply a function to all elements of a sequence.
xform[@a,@b]: (@a+>@b) * seq of @a +> seq of @b
xform(f,s) == [ f(x) | x in seq s ]
post len RESULT = len s and
(forall i in set inds s & RESULT(i) = f(s(i)));
-- Fold (iterate, accumulate, reduce) a binary function over a sequence.
-- The function is assumed to be associative and have an identity element.
fold[@a]: (@a * @a +> @a) * @a * seq of @a +> @a
fold(f, e, s) == cases s:
[] -> e,
[x] -> x,
s1^s2 -> f(fold[@a](f,e,s1), fold[@a](f,e,s2))
end
--pre (forall x:@a & f(x,e) = x and f(e,x) = x)
--and forall x,y,z:@a & f(x,f(y,z)) = f(f(x,y),z)
measure size2;
-- Fold (iterate, accumulate, reduce) a binary function over a non-empty sequence.
-- The function is assumed to be associative.
fold1[@a]: (@a * @a +> @a) * seq1 of @a +> @a
fold1(f, s) == cases s:
[e] -> e,
s1^s2 -> f(fold1[@a](f,s1), fold1[@a](f,s2))
end
--pre forall x,y,z:@a & f(x,f(y,z)) = f(f(x,y),z)
measure size1;
-- Pair the corresponding elements of two lists of equal length.
zip[@a,@b]: seq of @a * seq of @b +> seq of (@a * @b)
zip(s,t) == [ mk_(s(i),t(i)) | i in set inds s ]
pre len s = len t
post len RESULT = len s and mk_(s,t) = unzip[@a,@b](RESULT);
-- Split a list of pairs into a list of firsts and a list of seconds.
unzip[@a,@b]: seq of (@a * @b) +> seq of @a * seq of @b
unzip(s) == mk_([ x.#1 | x in seq s], [ x.#2 | x in seq s])
post let mk_(t,u) = RESULT in len t = len s and len u = len s;
-- and s = zip[@a,@b](RESULT.#1,RESULT.#2);
-- Are the elements of a list distinct (no duplicates).
isDistinct[@a]: seq of @a +> bool
isDistinct(s) == len s = card elems s;
-- Create a string presentation of a set.
format[@a]: (@a +> seq of char) * seq of char * seq of @a +> seq of char
format(f,sep,s) == cases s:
[] -> "",
[x] -> f(x),
t ^ u -> format[@a](f,sep,t) ^ sep ^ format[@a](f,sep,u)
end
measure size4;
-- The following functions wrap primitives for convenience, to allow them for example to
-- serve as function arguments.
-- Concatenation of two sequences.
app[@a]: seq of @a * seq of @a +> seq of @a
app(m,n) == m^n;
-- Set of sequence elements.
setOf[@a]: seq of @a +> set of @a
setOf(s) == elems(s);
-- Measure functions.
size0[@a]: @a * seq1 of @a +> nat
size0(-, s) == len s;
size1[@a]: (@a * @a +> @a) * seq1 of @a +> nat
size1(-, s) == len s;
size2[@a]: (@a * @a +> @a) * @a * seq of @a +> nat
size2(-, -, s) == len s;
size3[@a]: seq1 of @a * seq1 of @a +> nat
size3(-, s) == len s;
size4[@a]: (@a +> seq of char) * seq of char * seq of @a +> nat
size4(-, -, s) == len s;
size5[@a]: (@a +> bool) * seq of @a +> nat
size5(-, s) == len s;
end Seq
Char.vdmsl
/*
A module that specifies and defines general purpose types, constants and functions over
characters and strings (sequences of characters).
All functions are explicit and executable. Where a non-executable condition adds value, it
is included as a comment.
*/
module Char
imports from Seq all
exports types struct Upper
struct Lower
struct Letter
struct Digit
struct Octal
struct Hex
struct AlphaNumUpper
struct AlphaNumLower
struct AlphaNum
struct Space
struct WhiteSpace
struct Phrase
struct PhraseUpper
struct PhraseLower
struct Text
struct TextUpper
struct TextLower
values SP, TB, CR, LF: char
WHITE_SPACE, UPPER, LOWER, LETTER, DIGIT, OCTAL, HEX, ALPHANUMUPPER, ALPHANUMLOWER, ALPHANUM, PUNCTUATION: set of char
UPPERS, LOWERS, LETTERS, DIGITS, OCTALS, HEXS, ALPHANUMUPPERS, ALPHANUMLOWERS, ALPHANUMS, PUNCTUATIONS: seq of char
functions toLower: Upper +> Lower
toUpper: Lower +> Upper
isDigit: char +> bool
isDigits: seq of char +> bool
isWhiteSpace: char +> bool
isWhiteSpaces: seq of char +> bool
trimWhite: seq of char +> seq of char
filterWhite: seq of char +> seq of char
definitions
types
Upper = char
inv c == c in set UPPER;
Lower = char
inv c == c in set LOWER;
Letter = char
inv c == c in set LETTER;
Digit = char
inv c == c in set DIGIT;
Octal = char
inv c == c in set OCTAL;
Hex = char
inv c == c in set HEX;
AlphaNumUpper = char
inv c == c in set ALPHANUMUPPER;
AlphaNumLower = char
inv c == c in set ALPHANUMLOWER;
AlphaNum = char
inv c == c in set ALPHANUM;
Space = char
inv c == c = SP;
WhiteSpace = char
inv ws == ws in set WHITE_SPACE;
Punctuation = char
inv c == c in set PUNCTUATION;
Phrase = seq1 of (AlphaNum|Space);
PhraseUpper = seq1 of (AlphaNumUpper|Space);
PhraseLower = seq1 of (AlphaNumLower|Space);
Text = seq1 of (AlphaNum|WhiteSpace|Punctuation);
TextUpper = seq1 of (AlphaNumUpper|WhiteSpace|Punctuation);
TextLower = seq1 of (AlphaNumLower|WhiteSpace|Punctuation);
values
SP:char = ' ';
TB:char = '\t';
CR:char = '\r';
LF:char = '\n';
WHITE_SPACE:set of char = {SP,TB,CR,LF};
UPPER:set of char = {'A','B','C','D','E','F','G','H','I','J','K','L','M','N','O','P','Q',
'R','S','T','U','V','W','X','Y','Z'};
UPPERS: seq of Upper = "ABCDEFGHIJKLMNOPQRSTUVWXYZ";
LOWER:set of char = {'a','b','c','d','e','f','g','h','i','j','k','l','m','n','o','p','q',
'r','s','t','u','v','w','x','y','z'};
LOWERS: seq of Lower = "abcdefghijklmnopqrstuvwxyz";
LETTER:set of char = UPPER union LOWER;
LETTERS:seq of char = UPPERS ^ LOWERS;
DIGIT:set of char = {'0','1','2','3','4','5','6','7','8','9'};
DIGITS:seq of Digit = "0123456789";
ALPHANUMUPPER:set of char = UPPER union DIGIT;
ALPHANUMUPPERS:seq of char = UPPERS ^ DIGITS;
ALPHANUMLOWER:set of char = LOWER union DIGIT;
ALPHANUMLOWERS:seq of char = LOWERS ^ DIGITS;
ALPHANUM:set of char = LETTER union DIGIT;
ALPHANUMS:seq of char = LETTERS ^ DIGITS;
OCTAL:set of char = {'0','1','2','3','4','5','6','7'};
OCTALS:seq of Octal = "01234567";
HEX:set of char = {'0','1','2','3','4','5','6','7','8','9','A','B','C','D','E','F'};
HEXS:seq of Hex = "0123456789ABCDEF";
PUNCTUATION:set of char = {',','.',';',':','-','/'};
PUNCTUATIONS: seq of Punctuation = ",.;:-/";
functions
-- Convert upper case letter to lower case.
toLower: Upper +> Lower
toLower(c) == LOWERS(Seq`indexOf[Upper](c,UPPERS))
post toUpper(RESULT) = c;
-- Convert lower case letter to upper case.
toUpper: Lower +> Upper
toUpper(c) == UPPERS(Seq`indexOf[Lower](c,LOWERS));
--post toLower(RESULT) = c;
-- Is a character a decimal digit?
isDigit: char +> bool
isDigit(c) == c in set DIGIT;
-- Are all characters in a sequence decimal digits?
isDigits: seq of char +> bool
isDigits(sc) == forall c in set elems sc & isDigit(c);
-- Is a character white space?
isWhiteSpace: char +> bool
isWhiteSpace(c) == c in set WHITE_SPACE;
-- Are all characters in a sequence white space?
isWhiteSpaces: seq of char +> bool
isWhiteSpaces(sc) == forall c in set elems sc & isWhiteSpace(c);
-- Trim white space from the front and back of a string.
trimWhite: seq of char +> seq of char
trimWhite(s) == Seq`dropWhile[char](isWhiteSpace, reverse(Seq`dropWhile[char](isWhiteSpace, reverse(s))));
-- Filter white space from a string.
filterWhite: seq of char +> seq of char
filterWhite(s) == [ c | c in seq s & not isWhiteSpace(c) ];
end Char
VCParser.vdmsl
module VCParser
/***
VCParser
Author: Tomohiro Oda and Paul Chisholm
Version: 0.01
License: the MIT License
Copyright (c) 2013 Tomohiro Oda, Paul Chisholm
and Software Research Associates, Inc.
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in
all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
THE SOFTWARE.
***/
exports all
definitions
types
-- The source to be parsed - a sequence of characters.
SOURCE = seq of char;
-- Error meesage resulting from failed parsing.
ERROR :: message : seq of char;
-- Parse tree label (optional).
LABEL = [seq of char];
-- Parse tree: a label and a sequence of subtree/character items.
TREE :: label : LABEL
contents : seq of (TREE | char);
-- A parse result: the parse tree or error message, plus input text that was not processed.
PARSED :: parsed : TREE | ERROR
remaining : SOURCE;
-- The type of parsing functions.
PARSER = SOURCE -> PARSED;
values
/***
messages
***/
UNEXPECTED_EOF = "Unexpected EOF";
UNEXPECTED = "Unexpected ";
EXPECTED = "Expected ";
/***
parsers
***/
-- Recognise any character.
any =
lambda source : SOURCE &
cases source:
[] -> mk_PARSED(mk_ERROR(UNEXPECTED_EOF), source),
others -> mk_PARSED(mk_TREE(nil, [hd source]), tl source)
end;
-- Recognise a single white space character.
whiteChar =
label(
"whiteChar",
either([takeChar(" \t\r\n"(index)) | index in set {1, ..., 4}]));
-- Recognise a (possibly empty) sequence of white space characters.
whiteString = star(whiteChar);
-- Recognise a non-empty sequence of white space characters.
whiteString1 = plus(whiteChar);
-- Recognise and discard a (possibly empty) sequence of white space characters.
passWhiteString = pass(whiteString);
-- Recognise and discard a non-empty sequence of white space characters.
passWhiteString1 = pass(whiteString1);
-- Recognise a decimal digit.
digit =
label(
"digit",
either([takeChar("0123456789"(index)) | index in set {1, ..., 10}]));
-- Recognise a lower case roman alphabetic character.
lowerAlphabet =
label(
"lowerAlphabet",
either(
[takeChar("abcdefghijklmnopqrstuvwxyz"(index))
| index in set {1, ..., 26}]));
-- Recognise an upper case roman alphabetic character.
upperAlphabet =
label(
"upperAlphabet",
either(
[takeChar("ABCDEFGHIJKLMNOPQRSTUVWXYZ"(index))
| index in set {1, ..., 26}]));
-- Recognise a roman alphabetic character.
alphabet =
label("alphabet", either([lowerAlphabet, upperAlphabet]));
-- Recognise a natural number (leading zeroes not allowed).
natnum =
label(
"nat",
either(
[takeChar('0'),
concat(series([fail(takeChar('0')), concat(plus(digit))]))]));
-- Recognise an integer.
integer =
label("int", concat(series([option(takeChar('-')), natnum])));
functions
/***
parser generators
***/
-- Recognise a specified character.
takeChar : char -> PARSER
takeChar(c) ==
lambda source : SOURCE &
cases source:
[] -> mk_PARSED(mk_ERROR(UNEXPECTED_EOF), source),
others ->
if
hd source = c
then
mk_PARSED(mk_TREE(nil, [c]), tl source)
else
mk_PARSED(mk_ERROR(EXPECTED ^ "'" ^ [c] ^ "'"), source)
end;
-- Recognise and discard a specified character.
passChar : char -> PARSER
passChar(c) == pass(takeChar(c));
-- Recognise one of a sequence of specified characters.
takeOneOfChar : seq1 of char -> PARSER
takeOneOfChar(chars) ==
either([ takeChar(chars(i)) | i in set inds chars]);
-- Recognise a specified string.
takeString : seq1 of char -> PARSER
takeString(string) ==
concat(
series([takeChar(string(index)) | index in set inds string]));
-- Recognise and discard a specified string.
passString : seq of char -> PARSER
passString(s) == pass(takeString(s));
-- Recognise one of a sequence of specified strings.
takeOneOfString : seq1 of seq1 of char -> PARSER
takeOneOfString(strings) ==
either([ takeString(strings(i)) | i in set inds strings]);
/***
parser combinators
***/
-- Recognise, in order, a sequence of parsers.
-- VCParser: series([nonterm1,nonterm2,...,nontermn])
-- ISO 14977: nonterm1 , nonterm2 , ... , nontermn
series : seq1 of PARSER -> PARSER
series(parsers) ==
lambda source : SOURCE &
(let mk_PARSED(tree1, source1) = (hd parsers)(source)
in
cases mk_(tree1, tl parsers):
mk_(mk_ERROR(-), -) -> mk_PARSED(tree1, source1),
mk_(-, []) -> mk_PARSED(mk_TREE(nil, [tree1]), source1),
mk_(-, rest) ->
let mk_PARSED(tree2, source2) = series(rest)(source1)
in
cases tree2:
mk_TREE(-, trees2) ->
mk_PARSED(mk_TREE(nil, [tree1] ^ trees2), source2),
mk_ERROR(-) -> mk_PARSED(tree2, source2)
end
end);
-- Recognise one of a sequence of parsers.
-- VCParser: either([nonterm1,nonterm2,...,nontermn])
-- ISO 14977: nonterm1 | nonterm2 | ... | nontermn
either : seq1 of PARSER -> PARSER
either(parsers) ==
lambda source : SOURCE &
(let mk_PARSED(tree1, source1) = (hd parsers)(source)
in
cases mk_(tree1, tl parsers):
mk_(mk_ERROR(-), []) -> mk_PARSED(tree1, source1),
mk_(mk_ERROR(-), -) -> either(tl parsers)(source),
mk_(-, -) -> mk_PARSED(tree1, source1)
end);
-- Recognise a parser zero or more times.
-- VCParser: star(nonterm)
-- ISO 14977: { nonterm }
star : PARSER -> PARSER
star(parser) ==
lambda source : SOURCE &
cases parser(source):
mk_PARSED(mk_ERROR(-), -) -> mk_PARSED(mk_TREE(nil, []), source),
mk_PARSED(tree, rest) ->
if
rest = source
then
mk_PARSED(tree, rest)
else
(let mk_PARSED(mk_TREE(-, trees), source2) = star(parser)(rest)
in mk_PARSED(mk_TREE(nil, [tree] ^ trees), source2))
end;
-- Recognise a parser one or more times.
-- VCParser: plus(nonterm)
-- ISO 14977: nonterm , { nonterm }
plus : PARSER -> PARSER
plus(parser) ==
lambda source : SOURCE &
cases parser(source):
mk_PARSED(mk_ERROR(e), -) -> mk_PARSED(mk_ERROR(e), source),
mk_PARSED(tree, rest) ->
let mk_PARSED(mk_TREE(-, trees), source2) = star(parser)(rest)
in mk_PARSED(mk_TREE(nil, [tree] ^ trees), source2)
end;
-- Recognise a parser a specified number of times based on lower and upper bounds.
-- If lower bound omitted, 0 is assumed.
-- If upper bound is omitted, there is no limit.
iterate : PARSER * [nat] * [nat1] -> PARSER
iterate(parser, m, n) ==
let lower = if m = nil then 0 else m
in
series(
[parser | i in set {1, ..., lower}]
^ (if
n = nil
then
[star(parser)]
else
[option(parser) | i in set {lower + 1, ..., n}]))
pre m <> nil and n <> nil => m <= n;
-- Recognise a parser one or more times interleaved by a specified separator.
-- VCParser: iterateWithSeparator(nonterm1,nonterm2)
-- ISO 14977: nonterm1 , { nonterm2 , nonterm1 }
iterateWithSeparator : PARSER * PARSER -> PARSER
iterateWithSeparator(parser, separator) ==
let next_item = series([pass(separator), parser])
in series([parser, star(next_item)]);
-- Recognise a parser an exact number of times.
-- VCParser: iterateFixedTimes(nonterm,n)
-- ISO 14977: n * nonterm
iterateFixedTimes : PARSER * nat1 -> PARSER
iterateFixedTimes(parser, n) == iterate(parser, n, n);
-- Recognise a parser up to a specified number of times (lower bound is 0).
-- VCParser: iterateAtMost(nonterm,n)
-- ISO 14977: n * [ nonterm ]
iterateAtMost : PARSER * nat1 -> PARSER
iterateAtMost(parser, n) == iterate(parser, nil, n);
-- Recognise a parser at least a specified number of times (no upper limit).
-- VCParser: iterateAtLeast(nonterm,n)
-- ISO 14977: n * nonterm , { nonterm }
iterateAtLeast : PARSER * nat -> PARSER
iterateAtLeast(parser, n) == iterate(parser, n, nil);
-- Optionally recognise a parser.
-- VCParser: option(nonterm)
-- ISO 14977: [ nonterm ]
option : PARSER -> PARSER
option(parser) ==
lambda source : SOURCE &
cases parser(source):
mk_PARSED(mk_ERROR(-), -) -> mk_PARSED(mk_TREE(nil, []), source),
success -> success
end;
-- Recognise a parser, skipping preceding and succeeding blanks.
trimBlanks : PARSER -> PARSER
trimBlanks(parser) ==
concat(series([passWhiteString, parser, passWhiteString]));
-- Fail to recognise a parser.
-- If the parser succeeds, an error message is returned.
-- If the parser fails, success is returned and no input is consumed.
fail : PARSER -> PARSER
fail(parser) ==
lambda source : SOURCE &
(let mk_PARSED(tree1, source1) = parser(source)
in
cases tree1:
mk_ERROR(-) -> mk_PARSED(mk_TREE(nil, []), source),
mk_TREE(-, -) ->
mk_PARSED(
mk_ERROR(
UNEXPECTED
^ [source(index) | index in set {1, ..., len source - len source1}]),
source)
end);
-- Recognise a parser then concatenate all the items of any subtrees and lift into the top level tree.
concat : PARSER -> PARSER
concat(parser) ==
(lambda p : PARSED &
cases p:
mk_PARSED(mk_ERROR(-), -) -> p,
mk_PARSED(mk_TREE(-, contents), rest) ->
if contents = []
then mk_PARSED(mk_TREE(nil, contents), rest)
elseif is_(contents, seq of char)
then mk_PARSED(mk_TREE(nil, contents), rest)
else
mk_PARSED(
mk_TREE(
nil,
conc [let mk_TREE(-, subcontent) = contents(index) in subcontent
| index in set inds contents & is_(contents(index), TREE)]),
rest)
end)
comp parser;
-- Recognise a parser and discard the resulting parse tree.
pass : PARSER -> PARSER
pass(parser) ==
lambda source : SOURCE &
cases parser(source):
mk_PARSED(mk_TREE(l, -), rest) -> mk_PARSED(mk_TREE(l, []), rest),
err -> err
end;
-- Recognise a parser and assign a label to the resulting parse tree.
label : LABEL * PARSER -> PARSER
label(newLabel, parser) ==
(lambda parsed : PARSED &
cases parsed:
mk_PARSED(mk_TREE(-, contents), source) ->
mk_PARSED(mk_TREE(newLabel, contents), source),
others -> parsed
end)
comp parser;
-- Recognise a parser and, if successful, transform the parse result.
trans : (PARSED -> PARSED) * PARSER -> PARSER
trans(modifier, parser) == modifier comp parser;
-- Recognise a parser and, if successful, transform the parse tree.
transtree : (TREE -> TREE) * PARSER -> PARSER
transtree(modifier, parser) ==
trans(
lambda parsed : PARSED &
cases parsed:
mk_PARSED(mk_ERROR(-), -) -> parsed,
mk_PARSED(tree, rest) -> mk_PARSED(modifier(tree), rest)
end,
parser);
-- Recognise a parser; if it fails, set the error message.
iferror : seq of char * PARSER -> PARSER
iferror(message, parser) ==
trans(
lambda parsed : PARSED &
cases parsed:
mk_PARSED(mk_ERROR(-), rest) -> mk_PARSED(mk_ERROR(message), rest),
mk_PARSED(mk_TREE(-, -), -) -> parsed
end,
parser);
end VCParser
Numeric.vdmsl
/*
A module that specifies and defines general purpose functions over numerics.
All definitions are explicit and executable.
*/
module Numeric
imports from Char all,
from Seq all
exports functions min: real * real +> real
max: real * real +> real
formatNat: nat +> seq of Char`Digit
decodeNat: seq1 of Char`Digit +> nat
fromChar: Char`Digit +> nat
toChar: nat +> Char`Digit
zeroPad: nat * nat1 +> seq of Char`Digit
add: real * real +> real
mult: real * real +> real
definitions
functions
-- The minimum of two numerics.
min: real * real +> real
min(x,y) == if x<y then x else y;
-- The maximum of two numerics.
max: real * real +> real
max(x,y) == if x>y then x else y;
-- Format a natural number as a string of digits.
formatNat: nat +> seq of Char`Digit
formatNat(n) == if n < 10
then [toChar(n)]
else formatNat(n div 10) ^ [toChar(n mod 10)]
measure n;
-- Create a natural number from a sequence of digit characters.
decodeNat: seq1 of Char`Digit +> nat
decodeNat(s) == cases s:
[c] -> fromChar(c),
u^[c] -> 10*decodeNat(u)+fromChar(c)
end
measure len s;
-- Convert a character digit to the corresponding natural number.
fromChar: Char`Digit +> nat
fromChar(c) == Seq`indexOf[Char`Digit](c,Char`DIGITS)-1
post toChar(RESULT) = c;
-- Convert a numeric digit to the corresponding character.
toChar: nat +> Char`Digit
toChar(n) == Char`DIGITS(n+1)
pre 0 <= n and n <= 9;
--post fromChar(RESULT) = n
-- Format a natural number as a string with leading zeros up to a specified length.
zeroPad: nat * nat1 +> seq of Char`Digit
zeroPad(n,w) == Seq`padLeft[char](formatNat(n),'0',w);
-- The following functions wrap primitives for convenience, to allow them for example to
-- serve as function arguments.
-- Sum of two numbers.
add: real * real +> real
add(m,n) == m+n;
-- Product of two numbers.
mult: real * real +> real
mult(m,n) == m*n;
end Numeric
VCParserTest.vdmsl
module VCParserTest
imports from VCParser
types
ERROR renamed ERROR;
PARSED renamed PARSED;
TREE renamed TREE;
functions
takeChar renamed takeChar;
takeString renamed takeString;
series renamed series;
either renamed either;
star renamed star;
plus renamed plus;
option renamed option;
trimBlanks renamed trimBlanks;
fail renamed fail;
concat renamed concat;
pass renamed pass;
label renamed label;
trans renamed trans;
transtree renamed transtree;
iferror renamed iferror;
values
any renamed any;
digit renamed digit;
natnum renamed natnum;
integer renamed integer;
exports all
definitions
values
a = takeChar('a');
b = takeChar('b');
c = takeChar('c');
functions
id : PARSED -> PARSED
id(parsed) == parsed;
operations
test : PARSED * (PARSED->bool) ==> ()
test(parsed, result) == skip
pre result(parsed);
/* any */
test_any : () ==> ()
test_any() == (
test(any("a"), lambda p:PARSED & p.parsed.contents = "a");
test(any("1"), lambda p:PARSED & p.parsed.contents = "1");
test(any(""), lambda p:PARSED & is_ERROR(p.parsed)));
/* digit */
test_digit : () ==> ()
test_digit() == (
test(digit("a"), lambda p:PARSED & is_ERROR(p.parsed));
test(digit("1"), lambda p:PARSED & p.parsed.contents = "1");
test(digit(""), lambda p:PARSED & is_ERROR(p.parsed)));
/* natnum */
test_natnum : () ==> ()
test_natnum() == (
test(natnum("0"), lambda p:PARSED & p.parsed.contents = "0");
test(natnum("123"), lambda p:PARSED & p.parsed.contents = "123");
test(natnum("123.45"), lambda p:PARSED & p.parsed.contents = "123");
test(natnum("-1"), lambda p:PARSED & is_ERROR(p.parsed)));
/* integer */
test_integer : () ==> ()
test_integer() == (
test(integer("0"), lambda p:PARSED & p.parsed.contents = "0");
test(integer("123"), lambda p:PARSED & p.parsed.contents = "123");
test(integer("-123"), lambda p:PARSED & p.parsed.contents = "-123");
test(integer("123.45"), lambda p:PARSED & p.parsed.contents = "123");
test(integer("-x"), lambda p:PARSED & is_ERROR(p.parsed)));
/* takeChar */
test_takeChar : () ==> ()
test_takeChar() == (
test(takeChar('a')("abc"), lambda p:PARSED & p.parsed.contents = "a");
test(takeChar('a')("bca"), lambda p:PARSED & is_ERROR(p.parsed)));
/* takeString */
test_takeString : () ==> ()
test_takeString() == (
test(takeString("abc")("abcd"), lambda p:PARSED & p.parsed.contents = "abc");
test(takeString("abc")("abx"), lambda p:PARSED & is_ERROR(p.parsed)));
/* star */
test_star : () ==> ()
test_star() == (
test(star(a)("aabc"), lambda p:PARSED & len p.parsed.contents = 2);
test(star(a)("abc"), lambda p:PARSED & len p.parsed.contents = 1);
test(star(a)("bc"), lambda p:PARSED & len p.parsed.contents = 0));
/* plus */
test_plus : () ==> ()
test_plus() == (
test(plus(a)("aabc"), lambda p:PARSED & len p.parsed.contents = 2);
test(plus(a)("abc"), lambda p:PARSED & len p.parsed.contents = 1);
test(plus(a)("bc"), lambda p:PARSED & is_ERROR(p.parsed)));
/* option */
test_option : () ==> ()
test_option() == (
test(option(a)("aabc"), lambda p:PARSED & p.parsed.contents = "a");
test(option(a)("aabc"), lambda p:PARSED & p.remaining = "abc");
test(option(a)("abc"), lambda p:PARSED & p.parsed.contents = "a");
test(option(a)("abc"), lambda p:PARSED & p.remaining = "bc");
test(option(a)("bc"), lambda p:PARSED & p.parsed.contents = "");
test(option(a)("bc"), lambda p:PARSED & p.remaining = "bc");
);
/* concat */
test_concat : () ==> ()
test_concat() == (
test(concat(plus(a))("aaabc"), lambda p:PARSED & p.parsed.contents = "aaa");
test(concat(plus(a))("bc"), lambda p:PARSED & is_ERROR(p.parsed)));
/* trimBlanks */
test_trimBlanks : () ==> ()
test_trimBlanks() == (
test(trimBlanks(a)(" a bc"), lambda p:PARSED & p.parsed.contents = "a");
test(trimBlanks(a)(" a bc"), lambda p:PARSED & p.remaining = "bc");
test(trimBlanks(a)("a bc"), lambda p:PARSED & p.parsed.contents = "a");
test(trimBlanks(a)("a bc"), lambda p:PARSED & p.remaining = "bc");
test(trimBlanks(a)(" abc"), lambda p:PARSED & p.parsed.contents = "a");
test(trimBlanks(a)(" abc"), lambda p:PARSED & p.remaining = "bc");
test(trimBlanks(a)("bc"), lambda p:PARSED & is_ERROR(p.parsed)));
/* fail */
test_fail : () ==> ()
test_fail() == (
test(fail(a)("abc"), lambda p:PARSED & is_ERROR(p.parsed));
test(fail(a)("bc"), lambda p:PARSED & p.parsed.contents = "");
test(fail(a)("bc"), lambda p:PARSED & p.remaining = "bc"));
/* pass */
test_pass : () ==> ()
test_pass() == (
test(pass(a)("abc"), lambda p:PARSED & p.parsed.contents = "");
test(pass(a)("abc"), lambda p:PARSED & p.remaining = "bc");
test(pass(a)("bc"), lambda p:PARSED & is_ERROR(p.parsed)));
/* label */
test_label : () ==> ()
test_label() == (
test(label("A", a)("abc"), lambda p:PARSED & p.parsed.nodelabel = "A");
test(label("A", a)("abc"), lambda p:PARSED & p.parsed.contents = "a");
test(label("A", a)("abc"), lambda p:PARSED & p.remaining = "bc");
test(label("A", a)("bc"), lambda p:PARSED & is_ERROR(p.parsed)));
/* trans */
test_trans : () ==> ()
test_trans() == (
let parsed = mk_PARSED(mk_TREE(nil, []), []) in (
test(trans(lambda -:PARSED&parsed, a)("abc"), lambda p:PARSED & p = parsed);
test(trans(lambda -:PARSED&parsed, a)("bc"), lambda p:PARSED & p = parsed)));
/* transtree */
test_transtree : () ==> ()
test_transtree() == (
let tree = mk_TREE(nil, []) in (
test(transtree(lambda -:TREE&tree, a)("abc"), lambda p:PARSED & p.parsed = tree);
test(transtree(lambda -:TREE&tree, a)("bc"), lambda p:PARSED & is_ERROR(p.parsed))));
/* iferror */
test_iferror : () ==> ()
test_iferror() == (
test(iferror("A", a)("abc"), lambda p:PARSED & p.parsed.contents = "a");
test(iferror("A", a)("bc"), lambda p:PARSED & is_ERROR(p.parsed));
test(iferror("A", a)("bc"), lambda p:PARSED & p.parsed.message = "A"));
/* series */
test_series : () ==> ()
test_series() == (
test(series([a, b])("abc"), lambda p:PARSED & len p.parsed.contents = 2);
test(series([a, b])("bca"), lambda p:PARSED & is_ERROR(p.parsed)));
/* either */
test_either : () ==> ()
test_either() == (
test(either([a, b])("abc"), lambda p:PARSED & p.parsed.contents = "a");
test(either([a, b])("bca"), lambda p:PARSED & p.parsed.contents = "b");
test(either([a, b])("cab"), lambda p:PARSED & is_ERROR(p.parsed)));
traces
unit:
test_any();
test_digit();
test_natnum();
test_integer();
test_takeChar();
test_takeString();
test_star();
test_plus();
test_option();
test_concat();
test_trimBlanks();
test_fail();
test_pass();
test_trans();
test_transtree();
test_iferror();
test_series();
test_either();
combinators:
let c1, c2 in set {star, plus, option, trimBlanks, fail, pass} in
id(c1(c2(a))("abc"));
let n1, n2 in set {series, either} in
id(n1([n2([a, b]), c])("abc"));
let c1, c2 in set {star, plus, option, trimBlanks, fail, pass} in
let n1 in set {series, either} in
id(c1(n1([c2(a), b]))("abc"));
end VCParserTest