[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Strange problems
I have had this kind of problem where two formulas print the same but
are actually different. For example there could be append[U] in the
antecedent, and append[V] in the consequent. PVS does not always choose
the parameter instantiation that u would expect: it may be necessary to
provide it explicitely sometimes. Alternatively, it may be necessary to
prove some lemma, for example relating append[U] and append[V] in my
example.
I dont know of a PVS display feature that would let u see an expanded
version of the sequent with all the actuals, but it would be helpful to
debug this kind of situation.
In your case, I cannot tell which actual is different, but clearly this
is what happens.
Cheers!
pyg
Kellom{ki Pertti wrote:
>
> Maybe someone could help me out with this. I am developing a deep
> embedding of the DisCo (http://disco.cs.tut.fi) specification
> language. While trying to verify some properties of the DisCo
> language based on the embedding, I ran into the following sequent
> which PVS does not recognize to be provable:
>
> action_superposition.3.1.1.1.1 :
>
> [-1] sem(variable_assignments(role_of_object(ob!1, ra!1, roles(a!1)),
> append(new_fields(ref!1), fields(a!1)),
> append(new_assignments(ref!1), body(a!1))),
> ra!1, b!1)
> |-------
> [1] sem(variable_assignments(role_of_object(ob!1, ra!1, roles(a!1)),
> append(new_fields(ref!1), fields(a!1)),
> append(new_assignments(ref!1), body(a!1))),
> ra!1, b!1)
>
> I use subtypes in the specification, and I suspect this has something
> to do with that, but I have not been able to figure out what goes
> wrong here. At least the typepred command does not do anything useful,
> since it only adds antecedents into the sequent.
>
> The dump file is available at http://www.cs.tut.fi/~pk/tmp/dump and
> the relevant PVS file is superposition.pvs.
>
> Any help would be greatly appreciated.
> --
> pertti
--
Paul Y Gloess
E.N.S.E.R.B.: http://www.enserb.u-bordeaux.fr/~gloess
LaBRI: http://dept-info.labri.u-bordeaux.fr/~gloess