[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] semantic attachment problem
If you could give us a little more information about the semantic
attachment you are defining, we may be able to help.
In general, semantic attachments should only return basic types
(bool,reals,strings). Writing semantic attachments that return records,
datatypes, or closures is technically difficult and most of the time
unnecessary. Have in mind that semantic attachments are not a replacement
for the PVS specification language, but a mechanism to define, outside
PVS, uninterpreted functions that cannot be defined in PVS, e.g.,
input/output operations, floating point support for real-valued PVS
functions, non-deterministic functions such as RANDOM, etc.
PVSio already comes with an extensive library of pre-defined semantic
<PVSio> println("Hello World");
<PVSio> RANDOM = RANDOM;
Semantic attachments are only available through the PVSio interface for
animation purposes. You cannot use them in proofs, since they are
potentially unsound as the last example shows.
PVSio automatically imports all semantic attachments defined in a theory
and in all its imported theories.
Hope that this helps,
Cesar A. Munoz NASA Langley Research Center
Cesar.A.Munoz@xxxxxxxx Bldg. 1220 Room 115 MS. 130
http://shemesh.larc.nasa.gov/people/cam Hampton, VA 23681-2199, USA
Office: +1 (757) 864 1446 Fax: +1 (757) 864 4234
On 7/13/12 3:20 AM, "masoome parsa" <masoome.parsa@xxxxxxxxx> wrote:
>I am quite new in pvs. I have a pvs file which contains a theory. Then in
>pvs-attachment I wrote a defattach for one of the theories. I can see the
>result in ground evaluator. But In addition to the result , it gives me
>this message : Result not ground. Cannot convert back to PVS.
>The other problem is that how I can get the value of the defattach in my
>pvs file or at least in another lisp file that loads my pvs file !?