Axiomatic Language Example -- Calculator Program
Interactive addition & multiplication of decimal natural numbers
back to Axiomatic Language Home Page
1. Valid Expressions to be Defined
An interactive program that reads and writes lines of text can be specified
by valid expressions of the following form:
(Program <outs> <in> <outs> <in>
... <outs> <in> <outs>)
Here "<outs>" represents a sequence of zero or more output
lines typed by the program and "<in>" is a single input line
typed by the user. Each line is a sequence of expressions representing
characters.
(See elsewhere for axiomatic language syntax extensions.)
Each Program valid expression thus records a possible execution history.
We generate these valid expressions for all possible sequences of inputs
that the user might type. Thus the set of these valid expressions represent
all possible execution histories and can be considered a specification
of the external behavior of the interactive program.
This calculator program example is an interactive program that
evaluates simple arithmetic expressions in character strings,
such as "3+5*(6+1)", where our expressions
involve addition and multiplication of unsigned decimal numbers and
may be nested in parentheses. A decimal number result is returned
as the output of each input expression. A blank input line tells the
program to halt.
The program's final output line gives a count of the number of expressions
that were evaluated.
An example valid expression showing one possible execution history
for this calculator program is as follows:
(Program ("Enter expression to evaluate, empty line to halt:")
"2 + 3" -- user's input line
("5") -- program's output line
" 6*(1 + ( 5)) " -- spaces between tokens don't matter
("36")
"" -- blank input line tells program to halt
("Bye! -- 2 expressions evaluated")) -- final output line
Note that for this calculator program all the "<outs>" output
line sequences have exactly one output line.
This valid expression shows an example execution
where all the inputs are correct
expressions. The next section gives axioms that define Program valid
expressions for just correct inputs. The sections after that
give options for handling erroneous inputs.
2. Axioms for Correct Input Expressions
In this section we give axioms that generate Program valid
expressions, such as the one above, for evaluating arithmetic
expressions, but only for correct expressions. (Later sections will
address the issue of invalid inputs.)
First we give the top-level axioms for defining our Program valid
expressions:
! -- Axioms for Correct Input Arithmetic Expressions --
! Program - definition of Program valid expressions
(Program ("Enter expression to evaluate, empty line to halt:")
$dialog ! input & output lines
%blks ! an input line of blanks halts the program
(('Bye! -- ' $dec_count ' expressions evaluated')))<
(program_prefix $dialog %count),
(num>dec %count %dec_count), ! get count as decimal number
(blanks %blks).
! program_prefix - program dialog up to some point
! format: (program_prefix <outs> <in> ... <outs> <state>)
! -- here <state> is just the number of expressions evaluated
(program_prefix (`0)). ! initial state: 0 exprs evaluated
(program_prefix $dialog
%in ! next input expression
(%result) ! output value for expression
(`s $count)) < ! incremented count of # expressions
(program_prefix $dialog ($count)),
(eval %in %result). ! evaluate the expression
! eval - evaluate char string expression returning decimal value
(eval ($b1 $expr $b2) %result)<
(eval_expr ($expr) %num), ! get nat num value for char str expr
(num>dec %num %result), ! convert nat num to decimal string
(blanks ($b1 $b2)). ! blanks before & after expr
Next we give the axioms that define the evaluation of simple
arithmetic expressions in character strings:
! Grammar: E = E + T | T -- Expression
! T = T * P | P -- Term
! P = ( E ) | d{d} -- Primary (d is decimal digit)
! eval_expr - evaluate Expression
(eval_expr ($expr $b1 '+' $b2 $term) %enum+)< ! E = E + T
(eval_expr ($expr) %enum),
(eval_term ($term) %tnum),
(`plus %enum %tnum %enum+),
(blanks ($b1 $b2)).
(eval_expr ($term) %tnum)< ! E = T
(eval_term ($term) %tnum).
! eval_term - evalutate Term
(eval_term ($term $b1 '*' $b2 $primary) %tnum*)< ! T = T * P
(eval_term ($term) %tnum),
(eval_primary ($primary) %pnum),
(`times %tnum %pnum %tnum*),
(blanks ($b1 $b2)).
(eval_term ($primary) %pnum)< ! T = P
(eval_primary ($primary) %pnum).
! eval_primary - evaluate Primary
(eval_primary ('(' $b1 $expr $b2 ')') %enum)<
(eval_expr ($expr) %enum).
(eval_primary (%d $d) %num)<
(dec>num (%d $d) %num). ! one or more decimal digits chars
The utility functions blanks, num>dec, dec>num, `plus, and `times are
defined in this file.
3. Error Handling Approach #1 -- Let the Implementation Do It
In this section we give one approach to error handling -- let the
implementation do it.
For many problems, such as this calculator program, it is easier
to specify processing for correct inputs than to specify handling
incorrect inputs.
Since our implementation will be recognizing the correct inputs,
we can just let it provide a default error message whenever it
encounters an input that is not recognized as correct.
The invalid input (and resulting output error message) would be discarded
and it would be as if the invalid input had not occurred.
For this calculator program, an example execution history with an
invalid input might be as follows:
(Program
... -- valid inputs and outputs
"3 (2 + 1)" -- invalid input
("Error -- invalid input!") -- generic error message
... -- resume valid inputs and outputs
A sophisticated implementation might know exactly which character
in the input is the first that cannot correspond to a valid input.
It could then identify that character position in the output error message:
... -- valid inputs and outputs
"3 (2 + 1)" -- invalid input
(" ^ Error -- invalid input!") -- ^ points to 1st invalid char
... -- valid inputs and outputs
4. Error Handling Approach #2 -- Explicit Axioms for Invalid Inputs
In this section we give axioms for handling all the possible
invalid inputs for our calculator program. These axioms would be
added to the above axioms for valid inputs.
We first add two "program_prefix" axioms for error inputs:
! program_prefix - added axioms for invalid input error message
(program_prefix $dialog
($good_prefix %badch $anych) ! invalid input line with bad char
(($posblks '^ Error: ' $msg)) ! positioned error message
%count)< ! count of # evaluated exprs is unchanged
(program_prefix $dialog %count),
(eval_err ($good_prefix) %badch ($msg)),
(chars (%badch $anych)), ! only allow chars in input line
(blanks ($posblks)), ! blanks to position ^ under bad char
(=length ($good_prefix) ($posblks)).
(program_prefix $dialog
($incomplete) ! input line is not complete expression
! (but is a prefix of a valid expression, and thus has no bad char)
(($posblks '^ Error: ' $msg)) ! positioned error message
%count)<
(program_prefix $dialog %count),
(eval_err ($incomplete) ($msg)), ! premature eol instead of bad char
(member %nonblk ($incomplete)), ! incomplete expr contains a ...
(/= ' ' %nonblk), ! ... non-blank char
! -- Incomplete expr contains a non-blank char to exclude blank line
! input which tells the program to halt.
(blanks ($posblks)), ! blanks to position ^ at end-of-line
(=length ($incomplete) ($posblks)).
For our error handling we will use the following simplified grammar
with the error messages shown:
!/
Modified grammar for error handling:
E0 = E <eol> -- top-level expression ends with <end-of-line>
E = P {('+'|'*') P }
P = d{d} | '(' E ')'
d = '0'|'1'|...|'9' -- digits
Error cases:
E0 = E <eol>
^ ^
B 3
E = P {('+'|'*') P }
^ ^
A A
P = d{d} | '(' E ')' |
^ ^ ^
C 2or2' 1or1'
Error messages:
-- numbers are the actual messages, letters get propagated messages
-- we always skip leading blanks until next non-blank
(all the non-x characters exclude blank since we skipped past them)
1: non-digit,( char when primary expected
1': <eol> encountered when primary expected
2: non-),+,* char after expression in parentheses
2': <eol> encountered when right parenthesis expected
3: non-+,* char after top-level expression
-- propagated errors:
A: error (1,2) in primary P of expression E due to bad char
A': error (1',2') in primary P of expression E due to end-of-line
B: error (A = 1,2) in expression E of top-level expression E0 due to bad char
B': error (A' = 1',2') in expr E of top-level expr E0 due to end-of-line
C: error (A = 1,2) in nested expression E of primary due to bad char
C': error (A' = 1',2') in nested expr E of primary due to end-of-line
The possible errors are an invalid beginning of a primary, due to a
non-digit/non-( or end-of-line (errors 1 and 1') or an invalid
end of a nested expression, due to a non-), non-+/non-*, or end-of-line
(errors 2 and 2'), or invalid end of a top-level expression, due to
a non-+/non-* (error 3).
!\
The valid expression formats and axioms for the "eval_err" and
supporting predicates are as follows:
!/
Valid expression formats for error handling:
(eval_err <good prefix> <bad char> <err msg>) -- errors 1,2,3
(eval_err <good prefix but incomplete expr> <err msg>) -- errors 1',2'
-- good prefix may be null or all blanks
(eval_err_primary <good prefix> <bad char> <msg>) -- errors 1,2
-- incomplete primary due to bad character
(eval_err_primary <good prefix> <msg>) -- errors 1',2'
-- incomplete primary due to end-of-line
(eval_err_expr <good prefix> <bad ch> <msg>) -- error A
-- bad char before end of expression
(eval_err_expr <good prefix> <msg>) -- error A'
-- end-of-line before end of expression
!\
! axioms for error handling
! eval_err_primary - error in primary processing
! P = d{d} | '(' E ')' |
! ^ ^ ^
! C 2or2' 1or1'
(eval_err_primary ($b) %nondl "digit or left-parenthesis expected")< ! err 1
(blanks ($b)),
(not_member %nondl " 0123456789("). ! non-digit/non-left-paren ...
! ... as first non-blank of primary
(eval_err_primary ($b) "end-of-line encountered when expression expected")<
(blanks ($b)). ! err 1'
(eval_err_primary ($b '(' $expr_pre) %badch %msg)< ! err C
(blanks ($b)),
(eval_err_expr ($expr_pre) %badch %msg). ! nested expr has bad char
! good expr_prefix can have leading blanks
(eval_err_primary ($b '(' $expr_pre) %msg)< ! err C'
(blanks ($b)),
(eval_err_expr ($expr_pre) %msg). ! nested expr is incomplete
(eval_err_primary ($b1 '(' $b2 $expr $b3) %non+*r
"+ * or ) expected after nested expression")< ! err 2
(blanks ($b1 $b2 $b3)),
(eval_expr ($expr) %val), ! a good, complete expression
(not_member %non+*r " +*)"). ! non + * ) after nested expression
(eval_err_primary ($b1 '(' $b2 $expr $b3)
"input ends before right parenthesis")< ! err 2'
(blanks ($b1 $b2 $b3)),
(eval_expr ($expr) %val). ! a good, complete expression
! eval_err_expr - error in expression processing
(eval_err_expr ($prim_pref) $badch %msg)< ! 1st err A,A'
(eval_err_primary ($prim_pref) $badch %msg).
! -- string var for bad char lets it be optional!
(eval_err_expr ($b1 $expr $b2 %op $prim_pref) $badch %msg)< ! 2nd err A,A'
(eval_expr ($expr) %val), ! a good, complete expression
(member %op "+*"), ! + or * operator
(blanks ($b1 $b2)),
(eval_err_primary ($prim_pref) $badch %msg), ! 2nd primary has error
! -- recall that primary prefix has leading blanks
! eval_err - error in top-level expression
(eval_err ($expr_pref) $badch %msg)< ! err B,B'
(err_err_expr ($expr_pref) $badch %msg).
! top-level expression encounters bad char or premature end-of-line
(eval_err ($b1 $expr $b2) %non+*
"invalid char in top-level expression")< ! err 3
(eval_expr ($expr) %val), ! a valid, complete expression
(blanks ($b1 $b2)),
(not_member %non+* " +*").
! (See separate utilities source file for definitions of member,
! not_member, =length, chars, blanks.)
One observation is that the error handling is much more complicated
-- and more error prone -- than specification for valid inputs.
(It is likely that the above axioms have errors.)
An alternative approach to specifying correct expressions,
such as using a type of recursive descent parser, may be a better
way to guarantee complete coverage of all the invalid cases.
5. Error Handling Approach #3 -- Using Extended Axiomatic Language
In section 1 we defined an "eval" function that computes the value
of arithmetic expressions for valid inputs:
(eval <valid_input> <result>)
In section 4 we defined an "eval_err" predicate that (hopefully) covered
all the invalid inputs and for each gave an error message:
(eval_err <valid_prefix> <bad_char> <msg>)
(eval_err <incomplete_input> <msg>)
In this section we provide a simpler definition of the "eval_err"
predicate using extended axiomatic language.
Our definition only provides a generic error message, but we avoid the
complexity of having to define the complement of a context-free grammar.
Our extended axiomatic language axioms are as follows:
! -- Extended Axiomatic Language Definition of eval_err Predicate --
! eval_input - the set of valid inputs
(eval_input %input)< (eval %input %result).
! eval_prefix - the set of prefixes of valid inputs
(eval_prefix ($prefix))< (eval_input ($prefix $suffix)).
! eval_err - bad character makes valid prefix invalid:
(eval_err ($good_prefix) %badch "invalid character in input")<
(eval_prefix ($good_prefix)), ! prefix is valid
(eval_preifx ($good_prefix %badch))~. ! prefix + bad char is not valid
! the ~ marks a "complementary condition"
! eval_err - input is incomplete:
(eval_err ($incomplete) "input is not complete expression")<
(eval_prefix ($incomplete)), ! input is prefix of a valid input
! (thus there is no bad character in the incomplete input)
(eval_input ($incomplete))~. ! but input alone is not valid
These definitions are independent of the grammar for our arithmetic
expressions.
The challenge would be the greater difficulty of implementing
extended axiomatic language.