[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

2 Questions


I'm working with PVS as a backend to a proof obligation
generator and going through a case study right now.
There are two questions which I would like to place here:

1. I encounter problems with the TCCs generated for my
   obligations: due to the automatic process of generation
   I do not have any influence concerning the order
   of subcomponents of a formula. Since PVS only considers
   those subcomponents that preceed the one that induces
   the TCC are used as permise for the proof I have TCCs
   which I can't prove since the relevant information is
   standing after that.

      ( A AND P(front(x)) AND NOT (empty?(x)) )
    where x is an element of a list type
    supposes me to prove
        A => not (empty? (x))
    which I usually can't do without the additional information.

  Has anyone encountered similar problems? Has anyone found
  a solution? 
  Sam, did you consider any options for this?

2. A more basic technical problem:
   I would like to replace a single occurrence of a term
    in a formula that contains multiple occurrences of the
   term. I couldn't find a way of using expand, rewrite or
   replace for this.

   More concrete:

     I have a lemma  l = r
     and a formula
                     f (g(l), h(l))

     and I would like to replace only  the occurrence of l in
     "g(l)" with r. 

     Is there a possibility to do this?
     As far as I found rewrite and replace do not allow to
     select specific subterms, whereas expand expects a name
     to be replaced. 

Bettina Buth

| Dr. Bettina Buth                     | Tel. : ++49-421-218-2955            |
| FB 3 Informatik                      | Fax  : ++49-421-218-3054            |
| Bremen University, p.o. box 330 440  | email: bb@informatik.uni-bremen.de  |
| D-28334 Bremen, Germany              |                                     |