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

[Fwd: Re: [PVS-Help] Semantic attachments for evaluating quantifiers]


> As of now, I'm trying the following:
> exists?(s:set[t],f:pred[(s)):bool = exists (elt:(s)): f(s)
> I think this should let me attach semantics to exists? as well as to
> straight-a-way use quantifiers (here, exists) as defined in PVS while
> working out proofs. I'll use exists? instead of exists everywhere. Can
> I not use both my semantic attachments and PVSio together? For the
> things that are not evaluable in PVS and not defined in PVSio, I'll
> have to give semantic attachments.

In you are loading PVSio, you should use PVSio semantic attachments. For
example, if you have defined exists? in the theoy <dir>/MyTh.pvs, then
you can define your own semantic attachment for exists? in the file

(defattach |MyTh.exists?| (s f)
   "My own exists"

where ... is the lisp code defining exists?. This is what I call a PVSio
semantic attachment.  This mechanism is simpler and safer than writing
semantic attachments in .pvs.lisp (no need to "push", no need to know if
you should use pvs_ or pvs__, etc).  Check the documentation in
where I have more examples. Please use the latest version of PVSio
[PVSio-2.a (01/11/05)].

> Another question related to PVSio and attachments. Can I use PVSio
> functions in semantic attachments? I see it's not possible. For
> example, I want to get a "new" string which is not already there in
> the given set of strings. And I've axiomatized the function new but
> for animating, I would like to get input from user and I "don't" want
> to modify the original theory (as I want the animation to be
> transparent to the user). So the only (?) option is to give a sematic
> attachment:
> (push '|new| ...)
> (defun |pvs_new| (strings)
> (query_word "Please give a new string: ")
> ;; Validate that the string is not in "strings" )
> As this won't work, I copy the code of query_word instead:
> (defun |pvs_new| (string)
> (prompt "Please give a new string: ")
>   (format nil "~a" (read-token *standard-input* ""))
> ;; Validate that the string is not in "string")
> Is this the way to go? I believe there should be a better way.

There are better ways to do that. The one I prefer is called Theory
Intrepretations and it is also explained in the documentation.

Animation via theory interpretations

Assume that you have defined


  new(l:list[string]) : string

  ids : list[string] = (: "one", "two", "three" :)

  newids : list[string] = cons(new(ids),ids)


Now, you want to animate MyTh without modifying MyTh. Then, you create a
new theory, e.g., MyThaux, with some PVSio code defining new:

MyThaux : THEORY

  new(l:list[string]): string =
    let str = ref[string](query_word("Enter a string:")) in
    prog(while (member(val(str),l),
                            " already exists. Enter a new string:"))),

END MyThaux

Finally, you create the "main" theory for your animation, e.g., MyThio:



  io : THEORY = MyTh{{new := MyThaux.new}}

END MyThio

In this case, you are given an interpretation to new, without modifying
the original theory. To animate MyThio go to PVSio:

<PVSio> ids;
(: "one", "two", "three" :)

<PVSio> newids;
Enter a string:
one already exists. Enter a new string:
(: "uno", "one", "two", "three" :)

Actually, you can animate the specification directly from the command
line (without explicitly loading PVS):

$ pvsio MyThio:newids
Enter a string:
two already exists. Enter a new string:
(: "dos", "one", "two", "three" :)

Animation via defattach
Now, if you want to write your own semantic attachment for new (without
the theory interpretation mechanism),  create a file pvs-attachments in
your current directory

;;; pvs-attachments
(defattach MyTh.new(ls)
  "Returns a string that is not in ls"
  (let ((s (pvsio_stdio_query_line_1 "Enter a new string:")))
    (if (find s ls :test #'string=)
        (|pvsio_MyTh_new_1| ls)

Note that the name of the function in Lisp is different from the name of
the semantic attachment, e.g.,

* The semantic attachment MyTh.new is called |pvsio_MyTh_new_1| in Lisp
(bars is to force the use of uppercase for the identifier MyTh as by
default Lisp is case insensitive)

* stdio.query_line is called pvsio_stdio_query_line_1 in Lisp

To get the name in Lisp of a PVSio semantic attachment use the Emacs
command M-x help-pvs-attachment and then type the name, e.g.,
query_line.  Alternative, you can get this information using the PVSio

<PVSio> help_pvs_attachment("query_line");
Semantic attachments named query_line

Attachment: stdio.query_line

Usage: query_line(mssg)

Documentation: Queries a line from standard input with prompt MSSG

Lisp name : pvsio_stdio_query_line_1

Lisp definition:

(progn (prompt mssg) (format nil "~a" (read-line)))

Finally, to animate MyTh:

$ pvsio MyTh:newids
Enter a new string:
Enter a new string:
(: "uno", "one", "two", "three" :)

Final Remark
The definition of a semantic attachment for exists? is not trivial! The
major difficulty is that at the Lisp level you have to deal with a lisp
structure for your PVS objects. That structure is generated by the
ground evaluator and it's different from the CLOS representation of PVS
objects. For instance, that structure *does not* contain type

The simplest way to deal with it. Is to give let exists? uninterpreted
and then write an interpretation in PVS (via theory interpretations)
that uses lists instead of sets. In contrast to sets, you *can* animate
quite easily list functions.

Hope that all this helps,


Cesar A. Munoz H., Senior Staff Scientist
National Institute of Aerospace
144 Research Drive
Hampton, VA 23666, USA
Tel. +1 (757) 766 1539 Fax +1 (757) 766 1855