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

Re: [PVS-Help] PVS Help (fwd)

Hello Purnendu Sinha,

This is an old spec, and it looks like the LaTeX is not quite right.
What it used to have for the measure is

  MEASURE (LAMBDA pset, R, OldAccuse -> nat : R)

But this is no longer legal syntax.  The correct syntax is
  MEASURE (LAMBDA pset, R, OldAccuse : R)

Although you can also shorten this to


I have an older version of the spec, as well as it's supporting
theories.  I want to check with one of the authors; if it is OK with him
I will send it to you shortly.

Sam Owre

Dr. Purnendu Sinha <sinha@encs.concordia.ca> wrote:

> Hello,
> I am trying to work with a PVS theory that appeared in the paper "Formally
> Verified On-Line Diagnosis" by Walter, Lincoln and Suri. As the PVS source
> is not available, I tried to reproduce the code from latex-ified code
> which appears in the paper. A pvs file is attached to this mail.
> I am running into problems as described below:
> 1. While doing type-check (M-x tcp), it always gives an error ", expected
> here". But I do not see a need for "," in line 102. (part of MEASURE...)
> 2. Also, if I change MEASURE to something different to get pass that
> error, it then complains about the theories that are being imported.
> I am using PVS 3.1 running on Solaris. I would appreciate if you could
> guide me to resolve this problem.
> It would be much appreciated if a complete dump file with a complete proof
> could be provided.
> Thanks in advance.
> Best regards,
> Purnendu Sinha