Chapter 5. SPECIFICATION

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.

5.1 DESCRIPTION OF ADTS

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].

5.2 SPECIFICATION OF FUNCTIONS

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.

5.2.1 Notes about the specification

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.

5.2.2 Functions not formally defined

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.

5.2.3 Abstract Data Type

NAME

program(state)

SETS

AEset of Author Error messages = { ael, ae2, ae3, ae4, ae5, ae6, ae7, ae8, ae9, ae10, aell, ael2 }
Bset of boolean values, = { true, false }
BLANKTESTset of blank test options, = B
Cset of main window cursor column positions
CASETESTset of case test options, = B
CHARset of characters
CURRENTMPset of current match test values = (BLANKTEST × CASETEST × PUNCTTEST × SPELLTEST)
DEFAULTMPset of default match test values = (BLANKTEST × CASETEST × PUNCTTEST × SPELLTEST)
HEADWIDTHset of header window widths
MAINWIDTHset of main window widths
MAXROWSset of possible maximum rows for main window
MESSWIDTHset of message window widths
MPset of match parameters { BLANK, CASE, PUNCT, SPELL, ALL, NONE, DEF }
MRset of match results { MATCH, NOMATCH, NOANS, HELPREQ, OPTI, OPT2, OPT3, OPT4, OPT5, OPT6, PM1, PM2, PM3, PM4, PM5, PM6, PM7, PM8, AE }
PUNCTTESTset of punctuation test options, = B
Rset of main window cursor row positions
Sset of strings = CHAR+
SPACINGset of allowed blank rows between multiple-choice options, = {0, 1, 2}
SPELLTESTset of spell test options, = B
STATEset of states, = ( HEADER × MAIN × MESSAGE × R × C × DEFAULTMP × CURRENTMP × HEADWIDTH × MAINWIDTH × MESSWIDTH × MAXROWS × SPACING × MAXANSLEN )
WCARDset of wildcards = { * }
WCHARset of wildcharacters = { ? }
Zset 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.

Author Error messages

[] 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.

FUNCTIONS

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

SEMANTICS

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