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

[PVS-Help] PVS ground evaluator print output



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