[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification build
enrich build-base with
   
   procedures 
      build_rec#  int : list × treeorfail nonfunctional;
      build#  list : treeorfail nonfunctional;
declaration 
   build-rec
   : build_rec# (d; x, to)
       { 
          if is_empty(x)
          then to := fail
          else let h = head(x)
               in if h < d
                  then to := fail
                  else if h = d
                       then { 
                               x := pop(x) ; to := some(Leaf)
                            }
                       else let to0 = fail, to1 = fail
                            in { 
                                  build_rec#(d + 1; x, to0) ; 
                                  if to0 = fail
                                  then to := fail
                                  else { 
                                          build_rec#(d + 1; x, to1) ; if to1 = fail
                                          then to := fail
                                          else to := some(Node(to0 .t, to1 .t))
                                       }
                               }
       };
   build : build# (x; to)
             { 
                build_rec#(0; x, to) ; if ¬ is_empty(x)
                then to := fail
             };
   
end enrich