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

Re: [PVS-Help] PVS ground evaluator print output



Long,
You may want to look into PVSio, a PVS package that provides a simpler
interface to the ground evaluator and semantic attachments. It's already
included in the latest version of PVS. Unfortunately, some files are missing
in the current release. The missing files and instructions on how to use
PVSio are available here:

  http://shemesh.larc.nasa.gov/people/cam/PVSio/

Hope that it helps,

Cesar
On 4/24/10 6:59 PM, "Long Duong" <long@redphonesecurity.com> wrote:

> Hi,
>  
> Iım following this paper posted on the SRI site concerning semantic attachment
>  
> http://pvs.csl.sri.com/papers/eval-report/attach.pdf
>  
> and have a beginnerıs question.  Iım following the Section 2.2 printing theory
>  
> printing[T:TYPE+]: THEORY
> BEGIN
>   print(a: T):bool = true
> END printing
>  
> and trying to execute the ground evaluator executable statement
>  
> <GndEval> ³FORALL (x:upto(10)): print(id(x))²
>  
> but I fail to get the output result as in the paper of
>  
> 0 1 2 3 4 5 6 7 8 9 10
>  
> Instead I just get the returned TRUE value of the print function.  Iım running
> the pvs-allegro 4.2 binary version.
>  
> Please help, thanx.
> Long
>  
>  
>  
>