Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Date: Wed, 19 May 93 11:08:56 EDT
From: shb@oracorp.com
Message-Id: <9305191508.AA07266@sparta.oracorp.com>
To: info-hol@ted.cs.uidaho.edu
Subject: HOL90 style question

Using HOL90, and Compat.new_axiom, I just finished specifying and
proving some security properties of a model of an operating system.
There were several functions (e.g., the one checking whether sufficient
memory is available to create a new process) that weren't specified in
the model, but taken as undefined primitives.  In showing security
properties, though, I had to make minimal assumptions about these
undefined functions (e.g., that the new_process function returns a
process that is really new), and decided that using axioms was the most
straightforward way to make these assumptions.

Still, I know that using axioms is generally considered bad form, and
had previously made a conscientious effort to avoid them.  Is there
another technique for straightforwardly noting assumptions about
undefined functions without using axioms?  If not, and if new_axiom
really is the best tool for the job I used it for, shouldn't HOL90 have
its own version of new_axiom, without requiring reference to HOL88?

Steve Brackin
ORA