A Minimal Specification Language



Walter W. Wilson


Computer Sciences Corporation

& The University of Texas at Arlington







July 27, 2000


Language Objectives


1.  pure specification language

      what, not how

      efficiency is ignored

      transformation is required


1.  minimal

      as small and simple as possible

      nothing built-in that can be defined


1.  meta-language

      able to imitate other languages and paradigms


An Informal Introduction


axiomatic language [1982]

= pure Prolog with revised syntax

+ higher-order generalization [HiLog]

+ "string variables"


syntax differences:


father(bill,X) (father Bill %x)


      predicate names moved inside parentheses

      commas replaced with blanks

      (expression) variables start with %


higher-order generalization:

      predicate names can be expressions, incl. variables

      variables can represent entire predicates


An Informal Introduction (cont.)


example "axioms":


(number 0).

(number (s %))< (number %).


(plus 0 % %)< (number %).

(plus (s %1) %2 (s %3)<

(plus %1 %2 %3).


example generated expressions:


(number (s (s (s 0))))


(plus (s 0) (s 0) (s (s 0)))


An Informal Introduction (cont.)


string variables:

      start with $

      match zero or more expressions in a sequence

      simpler list predicate definitions:


(append ($1) ($2) ($1 $2)).


(member % ($1 % $2)).


(reverse () ()).

(reverse (% $) ($rev %))<

(reverse ($) ($rev)).


example generated expressions:


(append (a) (b c) (a b c))


(member c (a b c))


(reverse (u v) (v u))


The Language


"axioms" generate "valid expressions"


an expression is:


an atom (symbolic constant),

an expression variable,

or a sequence of zero or more expressions and

string variables



atoms: `abc, `+, `X3

expression variables: %expr, %x

string variables: $str, $1

sequences: (), (`M %y), (`xyz () $ (`))

-- expressions and string variables separated by

blanks and enclosed in parentheses


The Language (cont.)


axiom: a conclusion expression and zero or more

condition expressions:


conclu < cond1, , condn.

conclu. ! a comment


axioms generate axiom instances by substitution:

-- an expression for an expression variable

-- a string of expressions and string variables

for a string variable


axiom instances generate valid expressions:

If all conditions of an axiom instance are valid,

then the conclusion is valid.


For example, axioms


(`a `b).

((%) $ $)< (% $).


generate valid expressions:


(`a `b)

((`a) `b `b)

(((`a)) `b `b `b `b)


Some Syntax Extensions




  'A'  =  (`char (`bit0 `bit1))


character strings:


( 'abc' ) = ( 'a' 'b' 'c' )


"abc" = ('abc') = ('a' 'b' 'c')




abc = (` "abc")


Higher-Order Examples


definition of relations and sets:


% < (valid $1 % $2).

(valid (father Sue Tom)

(father Bill Tom)

(father Jane Bill)).


(%set %elem)<

(finite_set %set ($1 %elem $2)).

(finite_set day

(Sun Mon Tue Wed Thu Fri Sat)).

! generates (day Thu)


combining valid expressions:



(all_valid % $)< % , (all_valid $).


(one_valid $1 % $2)< % .

(parent %x %y)<

(one_valid (mother %x %y)

(father %x %y)).


Higher-Order Examples (cont.)


representing axioms in expressions:


%conclu < (axiom %conclu $conds),

(all_valid $conds).


(axiom (sort %1 %2)

(permutation %1 %2)

(ordered %2)).


(axiom $axiom)<

(axiom_set $1 ($axiom) $2).




((times % 0 0)

(number %))

((times %1 (s %2) %3)

(times %1 %2 %x)

(plus %x %1 %3))


((length () 0))

((length (% $) (s %n))

(length ($) %n))




Higher-Order Examples (cont.)


map predicates to sequences of arguments:


((` ($rel '*')) $nulls)<

(zero_or_more () ($nulls)).

((` ($rel '*')) $argseqsx)<

((` ($rel '*')) $argseqs),

((` ($rel)) $args),

(distr ($args) ($argseqs)



(zero_or_more % ()).

(zero_or_more % (% $))<

(zero_or_more % ($)).


(distr () () ()).

(distr (% $) (($seq) $seqs)

((% $seq) $seqsx))<

(distr ($) ($seqs) ($seqsx)).


example valid expressions:


(day* (Sat Tue Tue))

(reverse* ((a b c) () (u v))

((c b a) () (v u))).


Meta-Language Examples


LISP-like expression evaluation:


(finite_set digit "0123456789").

(index %set %elem %index)<

(finite_set %set ($1 %elem $2)),

(length ($1) %index).


(eval (` (%digit)) %value)<

(index digit %digit %value).

(eval (` ($digits %digit)) %valuex)<

(eval (`$digits)) %value),

(index digit %digit %n),

(times %value (s (s (s (s (s

(s (s (s (s (s

0))))) ))))) %10val),

(plus %10val %n %valuex).


(eval (quote %expr) %expr).

(eval (%fn $args) %result)<

(eval* ($args) ($results)),

(%fn $results %result).


example valid expressions:

(eval (plus 12 (times 4 5)) (s ))

(eval (reverse (append (quote (a b))

(quote (c)))) (c b a))


Meta-Language Examples (cont.)


procedural language example (from original paper):


(function factorial (N) is

variables I FACT ; ! local vars


I := 0 ;

FACT := 1 ;

while I < N loop

I := I + 1 ;

FACT := FACT * I ;

end loop ;

end factorial return FACT).


! add axioms for language definition


example valid expression:


(factorial (s (s (s 0)))

(s (s (s (s (s (s 0)))))))


What This Language Does Not Have


1. non-logical operations


2. built-in predicates


3. built-in inequality

-- define inequality between character bit atoms,

then between characters,

then between character strings and symbols,

and finally between expressions containing symbols


4. negation

-- define negative predicates (ex. "not_member"),

or define negation-as-failure for encoded axioms


5. assert/retract -- a set of axioms is static


6. input/output -- defined by interpretation


Defining Programs by Interpretation


Defining a program with valid expressions:


(program <input> <output>)


The input/output expressions are interpreted as files.

(ex. sequence of lines, each a sequence of characters)


Example program to reverse lines in a text file:


(program %input %output)<

(reverse* %input %output).


Interactive program:


(program <output1> <input1>

<output2> <input2>



-- generate for all possible execution histories!


String Variable Elimination


String variable unification can have multiple mgu's:


example: (a $) and ($ a) yield $ = '', 'a', 'a a',

-- problem due to "non-tail" string variables, as in ($ a)


Eliminating non-tail string variables:


(..x.. $1 ..y..)


is replaced by


(..x.. $1x) ! new variable


with the following condition added:


(APPEND ($1) (..y..) ($1x))


Then add these axioms:


(APPEND () ($2) ($2)).

(APPEND (% $1) %2 (% $3))<

(APPEND ($1) %2 ($3)).


Final transformation: represent sequences as nested pairs

(analogous to Prolog representation of lists)




simple language






defining programs by interpretation


Future Work on Transformation


do example unfold/fold proofs


identify proof patterns


incorporate into rules and schemas


combine into transformation program

-- handle axioms that are instances of stored patterns


continue adding rules and generalizing

-- eventually able to handle most programs?