maxl_ax : THEORY
BEGIN
 IMPORTING list[real]

 maxl : [list->real]

 l : VAR list
 x : VAR real

 Maxl : AXIOM
   member(x,l) implies x <= maxl(l)

END maxl_ax

maxl_th : THEORY
BEGIN
 IMPORTING list[real]

 maxl(l:list) : RECURSIVE real = 
   cases l of 
     null : 0,
     cons(a,r) : max(a,maxl(r))
   endcases
   MEASURE l by <<

END maxl_th

test : THEORY
BEGIN


  IMPORTING maxl_th, 
            maxl_ax{{ maxl :=  maxl }}

  main : void =
    println("Testing the function maxl") &
    let s = query_line("Enter a list of real numbers:") in
    let l = str2pvs[list[real]](s) in
    let m = maxl(l) in
      println("The max of "+s+" is "+m)

END test