This chapter is in two parts; the first explains briefly the fundamentals of ADTs, which is the notation that is used in the second part to specify the functions.
The functions are formally specified using Abstract Data Types (ADT). So, what is an ADT? A few definitions follow:
In other words an ADT shows what is done, but not how it is done.
There now follows a simple example, which shows the features of ADT specifications and introduces the notation.
Problem: specify a function, doubleplus, which takes an integer between 1 and 100, and returns two values, the first being double the integer, and the second (integer + 5). If the function is supplied with an integer that is less than 1, or greater than 100, a message is generated.
NAME
doubleplus(integer)
SETS
Z set of integers
M set of messages, consisting of 'out of range'.
FUNCTIONS
doubleplus: Z → ( Z × Z ) ∪ M
SEMANTICS
pre-doubleplus(z) ::= true
post-doubleplus(z;r) ::=
if ( z ≥ 1 ) ∧ ( z ≤ 100 )
then r = (( z * 2 ),(z+5))
else r = 'out of range'
First comes NAME, which simply indicates that the abstract data type doubleplus is a collection of (or works with) a set of integers.
SETS, also known as SORTS, are the objects manipulated by the operations.
FUNCTIONS, also known as SYNTAX, says what can be done to the object types in SETS. In this case there is only one operation, but there can be many. The function name is followed by a colon, which acts as a delimiter between the name and the objects. Next is a list of the sets which the function uses (in this case a list of one, namely Z). The symbol → separates the input sets from the set of results returned, and the symbol ∪ represents union in set notation. Note that:
A ∪ B = one item from the union of sets A and B.
A × B = two items (an ordered pair), the first from set A, and the second from set B.
Any value that is changed or created as a result of an operation appears (as the name of the set to which it belongs) in the result component of the function definition.
So, doubleplus returns either an ordered pair of two integers ( Z × Z ), or a message (M).
SEMANTICS is the relationship between the sets and the functions which can be applied to them (in this case just one). The pre- and post-conditions represent what is true before and after an operation.
Pre-conditions show the function name (preceded by pre-), and following this, in brackets there are variables representing the source data (conventionally lowercase equivalents of the types declared in SETS). Finally there is a declaration of the condition that must be true for the operation to be valid. (The symbol ::= has the meaning 'is defined as'). In this case there are effectively no preconditions. Note that using the operation with say a character, or a real number, is not prohibited, but the results are undefined.
Post-conditions show the function name (preceded by post-). Following this, in brackets, are variables representing the source data and results. These are separated by a semi-colon. Finally there is the relationship between the source data and the result that is true after the operation has been completed.
There are two basic ways of defining ADTs. The constructive approach, (also known as the operational or abstract model), which is used in the preceding example, defines the semantics explicitly by relating each operation to an underlying model. This is in contrast to the axiomatic model which involves an implicit definition of meaning by relating operations to one another by the use of axioms. Neither method is inherently better than the other, and both methods are used in the following specifications. The axiomatic approach is used mainly with functions that manipulate strings, and the constructive approach with screen addressing functions.
One term that is used in the specification below, but not previously defined is invariant assertion. This simply states something that is always true, or holds in a given case, and can save a lot of unnecessary repetition.
This exposition of ADTs is extremely brief, and quite superficial; interested readers may wish to pursue the topic, and a suitable source is the first three chapters of Abstract Data Types [Thomas, Robinson, Emms, 1988].
At this stage it is appropriate to mention that the ADT specification will be used in the design/implementation of the functions. For the most part, the Requirements Document and the ADT specification say the same thing, although in a different form. However, since the ADT specification is in an algebraic form, it will be a considerable aid when the detailed design of the functions takes place. This is particularly true with the more involved functions, especially the matching functions. Moreover, the Requirements Document does not go into as much detail as the ADT, it gives only the surface view, whereas the ADT is one step closer to the logic of the algorithms that will be used.
Since all pre-conditions are true, they are not shown.
States are a collection of external variables which a function can change. The screen output, as well as global constants can be considered as variables for the purposes of specification.
Dot notation is used to indicate which items of state are being accessed, for example, state.r refers to a particular value of the main window row co-ordinates. Authors cannot directly access the state; they must do so by calling a command.
underscore represents value of state prior to execution of an operation (usually represented by a line over the word or value in question. Readers familiar with VDM will know it as hook).
If a function is used within another function, then the state is not shown in the called function. Without this convention, clarity is lost. The function alpha_match contains a good example:
removeblanks(removepunct(upper(string)))
would be written:
removeblanks(removepunct(upper(string),state),state),state)
The second version is certainly not as clear as the first.
An informal description precedes each function that is not described in the Requirements Document and/or the User Manual, except where the operation of the function is self-evident.
Comments are enclosed by /* and */ .
Double quotes are used to indicate the start and end of literal strings.
All ∧ should be taken as conditional AND. In other words, if any condition is false within a given predicate, then that predicate is false, and subsequent conditions in that predicate need not be evaluated.
All ∨ should be taken as conditional OR. In other words, if any condition is true within a given predicate, then that predicate is true, and subsequent conditions in that predicate need not be evaluated.
In practice, when the specification is converted to code, the sequence of conditions tested should be followed strictly, to prevent the evaluation of conditions whose result is undefined. For example, if a string, s, is empty, there is not much point in trying to evaluate say, head(tail(s)). Some languages would raise an error in this situation.
The following functions are not formally defined here, but they are used in the specification; informal descriptions are given.
exit is called by author_error; it simply exits the author's program, and returns control to the operating system.
goto transfers control to a specified section of the program.
head returns the first item from a list of items. If the list is empty, head(list) = NIL.
if executes a command, or set of commands, if a given condition holds.
isin takes an item and a list. It returns true if the item is in the list, or false otherwise.
keypress waits for any key to be pressed.
legalscmp checks that the match parameter list (argument) to the function setcurrentmp conforms to the syntax requirements, and is semantically meaningful. For example, the list ALL, NONE is nonsense, and would be rejected.
legalsmp checks that the match parameter list (argument) to the function set_match_params conforms to the syntax requirements, and is semantically meaningful.
length returns an integer corresponding to the number of items in a list.
linesin returns an integer corresponding to the number of screen lines that a string would occupy if it were displayed.
sequence executes a list of actions sequentially.
tail returns the tail of a list, that is, the list with the first item removed. If the list contains one item, then tail(list) = NIL, and if the list contains no items (ie NIL), then tail(list) is undefined.
write writes to the main screen area.
tokenise takes a string, and returns a list of strings, the first and last characters of each string in the list being spaces (there are no spaces within each string in the list).
Three functions that are discussed in the Requirements Document, but which are not specified (or implemented) are matchreal, matchinteger, and match_ordered. If they are to be specified at later date, then SETS will have to be altered. Specifically, number match parameters would have to be incorporated into the match parameters set, MP, and the related parts of STATE (ie DEFAULTMP and CURRENTMP). The match results set, MR, would need additional members, to cater for the results of the number match functions.
program(state)
| AE | set of Author Error messages = { ael, ae2, ae3, ae4, ae5, ae6, ae7, ae8, ae9, ae10, aell, ael2 } |
| B | set of boolean values, = { true, false } |
| BLANKTEST | set of blank test options, = B |
| C | set of main window cursor column positions |
| CASETEST | set of case test options, = B |
| CHAR | set of characters |
| CURRENTMP | set of current match test values = (BLANKTEST × CASETEST × PUNCTTEST × SPELLTEST) |
| DEFAULTMP | set of default match test values = (BLANKTEST × CASETEST × PUNCTTEST × SPELLTEST) |
| HEADWIDTH | set of header window widths |
| MAINWIDTH | set of main window widths |
| MAXROWS | set of possible maximum rows for main window |
| MESSWIDTH | set of message window widths |
| MP | set of match parameters { BLANK, CASE, PUNCT, SPELL, ALL, NONE, DEF } |
| MR | set of match results { MATCH, NOMATCH, NOANS, HELPREQ, OPTI, OPT2, OPT3, OPT4, OPT5, OPT6, PM1, PM2, PM3, PM4, PM5, PM6, PM7, PM8, AE } |
| PUNCTTEST | set of punctuation test options, = B |
| R | set of main window cursor row positions |
| S | set of strings = CHAR+ |
| SPACING | set of allowed blank rows between multiple-choice options, = {0, 1, 2} |
| SPELLTEST | set of spell test options, = B |
| STATE | set of states, = ( HEADER × MAIN × MESSAGE × R × C × DEFAULTMP × CURRENTMP × HEADWIDTH × MAINWIDTH × MESSWIDTH × MAXROWS × SPACING × MAXANSLEN ) |
| WCARD | set of wildcards = { * } |
| WCHAR | set of wildcharacters = { ? } |
| Z | set of integers |
| + | non-empty set of lists, thus eg MP+ = set of lists of MP, excluding the empty set |
note
HEADER, MAIN, and MESSAGE are not specified further, but informally, they are what the user sees on the screen (ie the screen display).
HEADWIDTH, MAINWIDTH, and MESSWIDTH would in the implementation be less than or equal to the number of screen columns available on the monitor. The windows themselves would probably be centred, but this is not mandatory.
Since S = CHAR+, if not (tail(s) = NIL) then head(tail(s)) ∈ CHAR.
HELPKEY ∈ S. It is used in the specification to return a unique string from getanswer, which indicates that help has been requested. In practice it would consist of just one character.
[] indicates that the content of the variable or state will be shown on the screen.
ael = Author error in clearbetween: illegal row parameters. Row values must be between 1 and [state.maxrows] inclusive, and rowl ≤ row2. You set: rowl = zl, row2 = z2.
ae2 = Author error in getanswer: length less than 1 or length+current position > border or length > maximum allowed length [maxanslen].
ae3 = Author error in header: length of text too long. Maximum [headwidth] characters allowed. The text contains [length(text)] characters.
ae4 = Author error in match_any: required number of matches is out of range (2 to 9).
ae5 = Author error in match_any: number of words in model is greater than the maximum allowed (9).
ae6 = Author error in match_any: required number of matches ([z]) is greater than the number of words ([words in model]) in the model answer.
ae7 = Author error in mc: Not enough screen lines to display all options. Use one of the clear functions to remove previous text.
ae8 = Author error in mc: length of an option is greater than maximum allowed ([state.mainwidth]).
ae9 = Author error in message: length of text too long. Maximum [state.messwidth] characters allowed. The text contains [length(s)] characters.
ae10 = Author error in putcursor: values out of range. Row must be between 1 and [state.maxrows] inclusive. Col must be between 1 and [state.mainwidth] inclusive. You set row = [zl], col = [z2].
ae11 (raised in the setcurrentmp function) = Author error in match parameter list of a matching function.
ael2 = Author error in set_match_params: illegal match parameter.
alphamatch: S × S × MP+ × STATE → MR
author_error: AE × STATE → STATE
clearall: STATE → STATE
clearbetween: Z × Z × STATE → STATE ∪ (AE × STATE)
cleardisplay: STATE → STATE
compare: S × S → B
compare_without_assist: S × S → B
createprogram: → STATE
findword: S × S × MP+ × STATE → MR
getanswer: Z × STATE → (S × STATE) ∪ (AE × STATE)
header: S × STATE → STATE ∪ (AE × STATE)
matchesin: S+ × S × MP+ × Z × STATE → Z
match_any: Z × S × S × MP+ → MR
match_to_next_wild: S × S
mc2: S × S × S × STATE → (MR × STATE) ∪ (AE × STATE)
mc3: S × S × S × S × STATE → (MR × STATE) ∪ (AE × STATE)
mc4: S × S × S × S × S × STATE → (MR × STATE) ∪ (AE × STATE)
mc5: S × S × S × S × S × S × STATE → (MR × STATE) ∪ (AE × STATE)
mc6: S × S × S × S × S × S × S × STATE → (MR × STATE) ∪ (AE × STATE)
message: S × STATE → STATE ∪ (AE × STATE)
pause: STATE → STATE
putcursor: Z × Z × STATE → STATE ∪ (AE × STATE)
removeblanks: S × STATE → S
removepunct: S × STATE → S
setcurrentmp: MP+ × STATE → STATE ∪ (AB × STATE)
set_match_params: MP+ × STATE → STATE ∪ (AB × STATE)
skiptill: CHAR × S → S
test: S × S → B
upper: S × STATE → S
post-alphamatch(sl, s2, mp+, state;r)::=
if length(s2) = 0 then r = NOANS
else if s2 = HELPKEY then r = HELPREQ
else sequence
(
setcurrentmp( mp+ )
(if test( removeblanks(removepunct(upper(sl))),
removeblanks(removepunct(upper(s2))) )
then r = MATCH
else r = NOMATCH )
)
author_error displays an error message on screen if an author makes a semantic error in his/her program code, such as trying to locate the cursor at column 75 on a 70 column window. It displays the message until the author presses a key, whereupon the screen is cleared, and the program will terminate.
post-author_error(ae, state; r)::=
r = sequence
(
(state.main = state.main [curvearrowright] ae [curvearrowright] "Press any key to continue…"),
keypress,
(state.main = empty ∧ state.r = 1 ∧ state.c = 1),
exit
)
/* the symbol [curvearrowright] is borrowed from VDM, where it represents
concatenation. The addition of characters to a screen display can be considered
as a concatenation, hence the reason for the use of this symbol. */
post-clearall(state;r)::= r = ( state.header = empty state.main = empty ∧ state.message = empty ∧ state.r = 1 state.c = 1 )
post-clearbetween(zl, z2,state; r)::=
if ( (zl < 1) ∨ (zl > state.maxrows) ∨
(z2 < 1) ∨ (z2 > state.maxrows) ∨ (zl > z2) )
then r = author_error(ael)
else
(
if ( (state.r ≥ z1) ∧ (state.r ≤ z2)
then r =
(state.main is cleared between rows zl and z2 inclusive
∧ state.r = zl ∧ state.c = 1)
if ( (state.r < zl) ∨ (state.r > z2) )
then r =
(state.main is cleared between rows zl and z2 inclusive
∧ state.r = state.r
∧ state.c = state.c)
post-cleardisplay(state;r)::= r= ( state.main = empty ∧ state.r = ∧ state.c = 1 )
Compare is a boolean function that is used by the spelling assistant to determine the relationship (if any) between an answer string and a model string. Multiple numbers of wildcards and wildcharacters are allowed in the model, there being no restriction on their location in the model. One typographical error (ie insertion, omission, transposition, substitution) for each segment of a model enclosed by wildcards/characters is allowed in each matching segment of an answer. (See also compare_without_assistant).
post-compare(sl,s2;r)::= r <==>
/* All strings created by the tokenise function end with a space.
wchar represents a wildcharacter, wcard represents a wildcard. These may
be embedded in a model string.
Since all ∨ and ∧ are conditional, errors will not arise due to
trying to take, for example, tail(tail (string)) when length(string) = 1.
*/
(
(head(sl) = head(s2) = space) /* match found */
∨ /* no error, continue */
( head(sl) = head(s2)) ∧ compare(tail(sl), tail(s2)) )
∨ /* wildcharacter */
(
(head(sl) = wchar ∧
(
/* end of string, and omission, but match found */
(head(tail(sl)) = head(s2) = space) ∨
compare(tail(sl), tail(s2)) /* continue */
)
)
∨ /* wildcard
( (head(sl) = wcard ∧
let ch_plusrest = skiptill( head(tail(sl)), s2) in
( ( /* skip garbage and compare
not (ch_plusrest = NIL) ∧
compare(tail(sl), ch_plusrest)
)
∨
( not (head(tail(tail(sl))) = NIL) ∧
/* first char of tail(sl) is not in tail(s2)—possible
omission, so try again with next char in tail (s1). match_to_n_w
because omission is an error. All other errors catered for using
previous predicate. */
let ch_pr2 = skiptill( head(tail(tail(sl))), s2) in
(
not (ch_pr2 = NIL) ∧
match_to_next_wild( tail(sl), ch_pr2)
)
)
∨
/* first character in ch_plusrest was not the first character of
required portion of s2, but was (part of) some garbage, which is
allowed with wildcards. It could not have been a space. Find next
section of ch_plusrest which starts with h(t(sl)) and try to match.
*/
compare( sl, skiptill( head(tail(sl)), tail(ch_plusrest) ))
)
)
∨ /* substitution */
match_to_next_wild( tail(sl), tail(s2) )
∨ /* omission */
(
head(tail(sl)) = head(s2) ) ∧
match_to_next_wild( tail(sl), s2)
)
∨ /* transposition */
(
(head(sl) = head(tail(s2))) ∧
(head(tail(sl)) = head(s2)) ∧
match_to_next_wild(tail(tail(sl)), tail(tail(s2)) )
)
∨ /* insertion */
(
(head(sl) = head(tail(s2)) ∧
(
/* insertion at end of string, match found */
(head(sl) = space)
∨
match_to_next_wild( sl, tail(s2))
)
)
)
compare_without_assistant is a boolean function that is used to determine the relationship (if any) between an answer string and a model string. Multiple numbers of wildcards and wildcharacters are allowed in the model, there being no restriction on their location in the model. No typographical errors (ie insertion, omission, transposition, substitution) are allowed. (See also compare.)
post-compare_without_assistant(sl,s2;r)::= r <==>
(head(sl) = head(s2) = space) /* match found */
∨ /* no error, continue */
(
(head(sl) = head(s2)) ∧
compare_without_assistant( tail(sl), tail(s2))
)
∨ /* wildcharacter
(
(head(sl) = wchar ∧
compare_without_assistant(tail(sl), tail(s2))
)
∨ /* wildcard */
(
(head(sl) = wcard ∧
let ch_plusrest = skiptill( head(tail(sl)), s2) in
( ( /* skip garbage and compare */
not (ch_plusrest = NIL) ∧
compare_without_assistant( tail(sl), ch_plusrest)
)
∨
/* first character in ch_plusrest was not the first character of
required portion of s2, but was (part of) some garbage, which is
allowed with wildcards. It could not have been a space. Find next
section of ch_plusrest which starts with h(t(sl)) and try to
match. */
compare_without_assistant( sl, skiptill( head(tail(sl)),
tail(ch_plusrest) ))
createprogram contains all the initialisation procedures, and sets up the required starting state.
post-createprogram(;r)::= r = state = ( state.header = empty ∧ state.main = empty ∧ state.message = empty ∧ state.r = 1 ∧ state.c = 1 ∧ state.defaultmp.blanktest = false ∧ state.defaultmp.casetest = false ∧ state.defaultmp.puncttest = false ∧ state.defaultmp.spelltest = false ∧ state.currentmp.blanktest = undefined ∧ state.currentmp.casetest = undefined ∧ state.currentmp.puncttest = undefined ∧ state.currentmp.spelltest = undefined ∧ /* the state variables below are allowed to take other values, but as far as the prototype implementation of the authoring functions is concerned, they will not. Therefore, absolute values have been assigned to them. */ state.headwidth = 80 ∧ state.mainwidth = 80 ∧ state.messwidth = 80 ∧ state.maxrows = 23 ∧ state.spacing = 1 ∧ state.maxanslen = 80 )
post-findword(sl, s2, mp+, state;r)::=
if length(s2) = 0 then r = NOANS
else if s2 = HELPKEY then r = HELPREQ
else sequence
(
setcurrentmp( mp+ ),
let csl = removepunct(upper(sl)) and
cs2 = removepunct(upper(s2)) and
wordlist = tokenise(cs2) in
(if head(wordlist) = NIL then r = NOMATCH
else
if (test( csl, head(wordlist)) ) ∨
(test( csl, tail(wordlist)))
then r = MATCH )
)
post-getanswer(z,state;r)::=
if( z > 0 ∧ z < state.maxanslen ∧
z+state.c < state.mainwidth )
then
sequence(
(draw line z chars long starting at current cursor) ∧
(r = input string, or HELPKEY if Fl is pressed) )
else r = author_error(ae2)
post-header(s,state;r)::= if (length(s) < state.headwidth) ∧ (not linesin(s) > 1) then r = (state.header = s) else r = author_error(ae3)
matchesin returns the number of words in s+ that can be matched with words in s.
post-matchesin(s+, s, mp+, z, state;r)::=
/* in implementation, the initial call to matchesin would be made with
z = 0 */
r = z = 0 <==> ( (head(s+) = NIL) ∧ (z = 0) )
r = z > 0 <==>
(
(head(s+) NIL) ∧ (z > 0) )
∨
(findword(head(s+), s, MP+) = MATCH) ∧
matchesin(tail(s+), s, MP+, z+l) )
∨
matchesin(tail(s+), s, MP+, z)
)
post-match_any(z,sl,s2,mp+,state;r)::=
let modellist = tokenise(sl) in
if ( z < 2 ) ∨ (z > 9 ) then r = author_error(ae4)
if length( modellist ) > 9 then r = author_error(ae5)
if length( modellist ) < 2 then r = author_error(ae6)
if length(s2) = 0 then r = NOANS
if s2 = HELPKEY then r = HELPREQ
let wordsfound = matchesin(modellist,s2,mp+,0) in
if wordsfound ≥ z then r = MATCH
if wordsfound = 0 then r = NOMATCH
else
(
if wordsfound = 1 then r = PM1
if wordsfound = 2 then r = PM2
if wordsfound = 3 then r = PM3
if wordsfound = 4 then r = PM4
if wordsfound = 5 then r = PM5
if wordsfound = 6 then r = PM6
if wordsfound = 7 then r = PM7
if wordsfound = 8 then r = PMB
)
match_to_next_wild looks for an exact match between sl and s2, and returns true if it finds one. If there is a wildcard or wildcharacter in sl, the function looks for an exact character match between the strings up to, but not including, this wildcard/character, whereupon it calls compare with the remainder of the strings.
post-match_to_next_wild(sl,s2;r) <==>
(
(head(sl) = head(s2) = space )
∨
( (head(sl) = head(s2)) ∧
match_to_next_wild(tail(sl), tail(s2)) )
∨
(head(sl) = wchar ) ∧ compare(sl,s2) )
∨
(head(sl) = wcard ) ∧ compare(sl,s2) )
/* This does stop immediately, because compare uses the tail of sl in
its comparison if head(sl) is wild */
post-mc2(sl,s2,s3,state;r)::=
(
if ( (state.r + linesin(sl) + (3 * (state.spacing+l)) +1) > state.maxrows)
then author_error(ae7)
if (length(s2) > state.mainwidth) ∨
(length(s3) > state.mainwidth)
then r = author_error(ae8)
else r = sequence
(
(display stem and options),
(state.message = "Up/down arrows to move bar, Enter to select,
Fl = HELP."),
(if s2 is selected then r =
(
OPT1 ∧
(state.r = (state.r + linesin(sl) +
(3 * (state.spacing+l)) +1) ) ∧
(state.c = 1)
)
(if s3 is selected then r =
(
OPT2 ∧
(state.r = (state.r + linesin(sl) +
(3 * (state.spacing+l)) +1) ∧
(state.c =1)
)
)
)
)
Note: mc3, mc4, mc5, mc6 are as mc2, with the number of options in the sequence equal to the number of strings less one.
post-message(s,state;r)::= if (length(s) < state.messwidth) ∧ (not linesin(s) > 1) then r = (state.message = s) else r = author_error(ae9)
post-pause(state;r)::=
r = sequence(
(state.message = "Press any key to continue…"
keypress,
(state.message = empty)
post-putcursor(zl,z2,state;r)::=
if (zl < 1) ∨ (z2 > state.maxrows)
(z2 < 1) ∨ (z2 > state.mainwidth)
then r = author_error(ae10)
else r = (state.r = zl ∧ state.c = z2)
post-removeblanks(s, state;r)::= if state.currentmp.blanktest = false then r = the string with blanks removed to leave one blank between words. else r = s
post-removepunct(s, state;r)::= if state.currentmp.puncttest = false then r = s without punctuation else r = s
setcurrentmp is similar in action to the set_match_params function, the chief difference being that it is used to set the current match parameters, which are used by the matching functions.
post-setcurrentmp(mp+ ;r)::=
if legalscmp(mp+)
then
(
if (head(mp+) = DEF)
then r = (state.currentmp = state.defaultmp)
if (head(mp+) = ALL)
then r =
(state.currentmp.blanktest = true ∧
state.currentmp.casetest = true ∧
state.currentmp.puncttest = true ∧
state.currentmp.spelltest = true )
if (head(mp+) = NONE)
then r =
(state.currentmp.blanktest = false ∧
state.currentmp.casetest = false ∧
state.currentmp.puncttest = false ∧
state.currentmp.spelltest = false )
if ( (not head(mp+) = ALL ) ∧
(not head(mp+) = NONE ∧
(not head(mp+) = DEF ) ) )
then r =
(
if isin(BLANK, mp+)
then state.currentmp.blanktest = true
else state.currentmp.blanktest = false
∧
if isin(CASE, mp+)
then state.currentmp.casetest = true
else state.currentmp.casetest = false
∧
if isin(PUNCT, mp+)
then state.currentmp.puncttest = true
else state.currentmp.puncttest = false
∧
if isin(SPELL, mp+)
then state.currentmp.spelltest = true
else state.currentmp.spelltest = false
)
)
else r = author_error(aell)
post-set_match_params(mp+;r)::=
if legalsmp(mp+)
then
(
if (head(mp+) = ALL) then r =
(state.defaultmp.blanktest = true ∧
state.defaultmp.casetest = true ∧
state.defaultmp.puncttest = true ∧
state.defaultmp.spelltest = true )
if (head(mp+) = NONE) then r =
(state.defaultmp.blanktest = false ∧
state.defaultmp.casetest = false ∧
state.defaultmp.puncttest = false ∧
state.defaultmp.spelltest = false )
if (not head(mp+) = ALL) ∧ (not head(mp+) = NONE)
then r =
(
if isin(BLANK, mp+)
then state.defaultmp.blanktest = true
else state.defaultmp.blanktest = false
∧
if isin(CASE, mp+)
then state.defaultmp.casetest = true
else state.defaultmp.casetest = false
∧
if isin(PUNCT, mp+)
then state.defaultmp.puncttest = true
else state.defaultmp.puncttest = false
∧
if isin(SPELL, mp+)
then state.defaultmp.spelltest = true
else state.defaultmp.spelltest = false
)
)
else r = author_error(ael2)
skiptill takes a character and a string, finds the first occurrence of the character in the string, and returns the rest of the string from that character inclusive onwards. If the character is not in the string, an empty string is returned.
post-skiptill(char,s;r)::=
if head(s) = NIL
then r = NIL
else
(
if char = head(s) then r = s
else r = (skiptill( char, tail(s)))
)
post-test(sl,s2;r = true) <==>
(
( (state.currentmp.spelltest = true) ∧
(compare_without_assistant(sl, s2) )
/* compare_without_assistant does not allow spelling errors */
∨
( (state.currentmp.spelltest = false ∧ compare(sl,s2) )
)
post-upper(s, state;r)::= if state.currentmp.casetest = false then r = uppercase version of s else r = s
Preface | Contents | 1 Introduction | 2 Review | 3 Req. analysis | 4 Req. documents | 5 Specification | 6 Design | 7 Verification | 8 Discussion | 9 PAL manual | Appendix A | Appendix B | Appendix C | Glossary | References | Index