ACL2 Model

What follows is the extemely simple ACL2 specification of CAETI systems developed for Model 1 as modified for Model 2. It is modified by replacing "TCP socket" terminology by "CAETI address" terminology.

The infix syntax should be clear, given the following operators:

(l \ a) finds the first pair in l whose first element equals a (assoc).
a :> l adds a to the front of list l (cons).
[a, b, c] contructs a list of three elements.

in-package "ACL2";

type a-caeti-address;

type a-CMA-type = enum[ tell, ask, do, subscribe, sorry ];

type a-CMA-msg =
 record (kind : a-CMA-type,
         sender : a-caeti-address,
         receiver : a-caeti-address,
         content  : string,
         language : string := "text",
         ontology : string,
         reply-with  : string,
         in-reply-to : string);

type a-CMA-history = a-CMA-msg * ;        /* A list of a-CMA-msg */

type an-in-out = record ( inl : a-CMA-history, outl : a-CMA-history );

/* a-caeti-system is defined to be an association list, mapping addresses to in-out  histories. */

type a-caeti-system = [ a-caeti-address . an-in-out ] *;

theorem caeti-system-true-list
 { a-caeti-system(x) -> true-listp(x) };

/* Find the pair in list l whose first element equals a. */
function is-unique-caeti-address (s : a-caeti-address, l : a-caeti-system) : boolean 
 { ~(l \ s) };

function all-caeti-addresss-unique (l)
{ if ~consp(l)
    then t 
  elif a-caeti-system(l) & is-unique-caeti-address(l.car.car, l.cdr)
    then all-caeti-addresss-unique(l.cdr)
  else nil };

verify guards all-caeti-addresss-unique;

function is-caeti-system (l : a-caeti-system) : boolean 
 { all-caeti-addresss-unique(l) };

ACL2 Model

This page is URL http://www.computationallogic.com/software/caeti/architecture/model/acl2-model.html