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

[PVS-Help] PVS ground evaluator print output



I’m following this paper posted on the SRI site concerning semantic attachment




and have a beginner’s question.  I’m following the Section 2.2 printing theory


printing[T:TYPE+]: THEORY


  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.