Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Date: Thu, 18 Jun 92 19:03:16 BST
From: Mike.Gordon@uk.ac.cam.cl
Message-Id: <9206181803.AA03040@dipper.cl.cam.ac.uk>
To: info-hol@edu.uidaho.cs.ted
Subject: Can anyone help?


Return-Path: <mike.gordon-request@uk.ac.cam.cl>
Date: Thu, 18 Jun 92 10:40:08 -0700
From: lamport@com.dec.src (Leslie Lamport)
To: horning@com.dec.Pa, guttag@edu.mit.lcs.larch, garland@edu.mit.lcs.larch, 
    saxe@com.dec.Pa, Mike.Gordon@uk.ac.cam.cl, rc@edu.cornell.cs, boyer@com.cli, 
    goldschlag@mil.ncsc.tycho, dmg@com.cli, meyer@EDU.MIT.LCS.theory, 
    jwright@fi.abo.finabo, hsr@dk.dth.id, Edmund.Clarke@EDU.CMU.CS.GP.G, 
    emerson@edu.utexas.cs, probst@ca.crim.bond, k@com.att.gauss, ma@com.dec.Pa, 
    dill@edu.stanford.amadeus, pw@be.ac.ulg.montefiore, sifakis@fr.imag
Cc: lamport@com.dec.Pa, urban@dk.aau.daimi, peter@dk.dth.id
Subject: request for help in automatic verification


This is a request for help in the automatic verification of one part of
TLA proofs--the computing of Enabled predicates.  Please pass it along
to anyone who might be interested or might have suggestions.

In TLA, an action is a boolean expression involving primed and unprimed
variables.  For any action A, Enabled(A) is the formula obtained by
existentially quantifying over the primed variables.  For example, let
A be the action

   \/ /\ x > y
      /\ x' = x + z 
      /\ y' = 5
   \/ /\ x < y
      /\ x' = x
      /\ y' = y

(I write disjunctions and conjuntions as lists of \/'s and /\'s, using
indentation to eliminate paretheses.)  Then Enabled(A) equals

   \exists a, b : \/ /\ x > y
                     /\ a = x + z 
                     /\ b = 5
                  \/ /\ x < y
                     /\ a = x
                     /\ b = y

TLA is an untyped logic, and all TLA operators are total.  The laws of
existential quantification imply the soundness of the following rules.

  1. Enabled(A \/ B) = Enabled(A) \/ Enabled(B)
  
  2. If A and B have no primed variables in common, then
     Enabled(A /\ B) = Enabled(A) /\ Enabled(B)
  
  3. If A has no primed variables, then Enabled(A) = A.
  
  4. If F has no primed variables, then
     Enabled(x' = F) = TRUE
  
  5.If F has no primed variables, then
      Enabled(x' \in F) =  F \neq \emptyset
  
  6. Enabled((x' = F) /\ A) = Enabled((x' = F) /\ A[F/x']) 
     where A[F/x'] is the action obtained by substituting
     F for x'.

Rules 1-5 are sufficient to calculate Enabled predicates for most of
the actions that one encounters in TLA formulas.  In the example above,
we get

Enabled \/ /\ x > y
           /\ x' = x + z 
           /\ y' = 5
        \/ /\ x < y
           /\ x' = x
           /\ y' = y 

   =  \/ Enabled /\ x > y            [by rule 1]
                 /\ x' = x + z 
                 /\ y' = 5
      \/ Enabled /\ x < y
                 /\ x' = x
                 /\ y' = y 
  
   =  \/ /\ Enabled x > y            [by rule 2]
         /\ Enabled x' = x + z 
         /\ Enabled y' = 5
      \/ /\ Enabled x < y
         /\ Enabled x' = x
         /\ Enabled y' = y 
  
   =  \/ /\ x > y            [by rules 3 and 4]
         /\ true
         /\ true
      \/ /\ x < y
         /\ true
         /\ true
  
   =  \/ x > y 
      \/ x < y

Rule 6 would be needed to compute something like

  Enabled /\ x' = 5 
          /\ y' = x'+1

I am looking for a system that can do one or both of the following:

  (a) Automatically compute Enabled predicates using rules 1-6
      (or perhaps just 1-5).
  
  (b) Automatically verify a formula of the form
        Enabled A  =  P
      where the verification follows from Rules 1-6 (or perhaps
      just 1-5) and trivial logic--commutativity of /\ and 
      \/, A \/ True = True, etc.

By automatic, I mean without human intervention, using input that could
be generated from the TLA formulas by a program.

Leslie Lamport