[SAL] Using recursive datatypes with model checker

mwwhalen at rockwellcollins.com mwwhalen at rockwellcollins.com
Tue Apr 17 11:49:46 PDT 2007

Hello all,

  Is it possible to use recursive types (e.g., list) defined as DATATYPEs
with the SAL model checking tools?  I tried creating a list datatype and
defining a couple of operations, but got errors of various sorts from the
different model checking tools (sal-smc, sal-inf-bmc) related to
finiteness.  Here's my small example:

listtest: CONTEXT =
   id: TYPE ;

   id_list : TYPE =
         node(hd: id, tl: id_list)
      END  ;

   IDL : id_list ;

   length: [id_list -> NATURAL] =
      LAMBDA (lst: id_list):
         IF nil?(lst) THEN 0 ELSE 1 + length(tl(lst)) ENDIF ;

   system : MODULE =
      OUTPUT out_L : id_list
      out_L = IDL ;
   END ;

   prop: THEOREM system |- G(length(out_L) < 5);


Obviously, I'm not constraining IDL so there are essentially an infinite
number of constants to check.  Are there any constraints that I can place
on the use of recursive datatypes (e.g., max size) in order to meet
finiteness constraints in SAL?  Anyone else tried to use recursive
datatypes and have any models lying around?

Thanks for your time!

:-) Mike

Dr. Michael Whalen
Rockwell Collins Inc.
7805 Telegraph Rd. Suite 100
Bloomington, MN 55438

RCI Office Phone: 319-263-2568
UMN Office Phone: 612-625-4543
Cell Phone: 651-442-8834

More information about the SAL mailing list