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

# Re: [PVS-Help] Hopefully Simple Proof Question

```Baldwin Rusty O Civ AFIT/ENGE wrote:
> Hello,
>
> I have what I hope is a simple question to help me dispatch a type check
> obligation.  Below is a pvs file that generates the tc OBLIGATION that
> follows it.
>
> I THINK what the obligation is telling me is that for all edges e I add,
> e`1 and e`2 are vertices in the graph AND e`1 /= e`2.
>
Yes, that is what it's saying.
> I'm not sure how to prove the first part (e`1 and e`2 are vertices) and
> I tried to use the commented out type TT to handle the second part
> (which it didn't).
>

You are on the right track.  When you define the four constants (x,y,z,
and zz) there is nothing
to say that they are different constants.  One way to solve this is to
explicitly say that z and zz are
different:

edge_test2: THEOREM
z /= zz
IMPLIES
edge?(a_graph)(x,y) AND edge?(a_graph)(z,zz)

You might also consider defining a_graph in the THEOREM itself, instead
of as a separate constant:

b_graph: VAR simple_digraph
edge_test3: THEOREM
b_graph = (# vert := add(zz, add(z, add(x,
singleton[T](y)))), edges := add((z,zz), singleton[pair](x,y)) #) AND
z /= zz
IMPLIES
edge?(b_graph)(x,y) AND edge?(b_graph)(z,zz)

Jeff
> Thanks for any insight.
>
> Rusty
>
> ===========
> jj [ T: TYPE+ ]
> 		: THEORY
>
>   BEGIN
>
> %   TT: TYPE+ = {a,b:T | a /= b}
>
>   IMPORTING digraphs@digraphs[T]
>
>    x, y, z, zz: T
>
>    a_graph: simple_digraph = (# vert := add(zz, add(z, add(x,
> singleton[T](y)))), edges := add((z,zz), singleton[pair](x,y)) #)
>
>    edge_test: THEOREM edge?(a_graph)(x,y) AND edge?(a_graph)(z,zz)
>
>
> End jj
> ============
> % Subtype TCC generated (at line 12, column 29) for
>     % (# vert := add(zz, add(z, add(x, singleton[T](y)))),
>     %    edges := add((z, zz), singleton[pair](x, y)) #)
>     % expected type  simple_digraph[T]
>   % unchecked
> a_graph_TCC1: OBLIGATION
>   (FORALL (e: edgetype[T]):
>      add[pair[T]]((z, zz), singleton[pair[T]](x, y))(e) IMPLIES
>       add[T](zz, add[T](z, add[T](x, singleton[T](y))))(e`1) AND
>        add[T](zz, add[T](z, add[T](x, singleton[T](y))))(e`2))
>    AND
>    (FORALL (e: edgetype[T]):
>       add[pair[T]]((z, zz), singleton[pair[T]](x, y))(e) IMPLIES e`1 /=
> e`2);
>
>

```