PVS applications

Paul Y Gloess

E.N.S.E.R.B. & LaBRI [C.N.R.S. UMR 5800]

may 3, 2000

All PVS libraries below have been developed with PVS 2.3; they probably work with patches currently available. For each library, the name of the dump has the form:

lib.day_month_year.theory.dump

where
Library dump
Description
compiler.14_january_2000.dump.dump
 Correctness of a simple compiler of algebraic expressions. More?
fol.28_november_1999.dump.dump
First order logic. More?
imperative.28_november_1999.dump.dump
Imperative programming, Hoare calculus. Requires "fol" library. More?
 permutations.18_april_2000.list_permutations.dump
Definition and properties of permutations (under construction). More?
wf.29_march_2000.wf_properties.dump
Properties of well founded relations. More?

Please feel free to use any of these libraries: thank you for referring to the URL of this page:

http://dept-info.labri.u-bordeaux.fr/~gloess/pvs/    .
For any question or suggestion, please write to me: Paul Y Gloess<Paul.Gloess@LaBRI.U-Bordeaux.Fr>.

Correctness of a simple compiler of algebraic expressions

This is a pedagogical example illustrating proof techniques for functional programming, and the newly available PVS ground evaluator. The compiler is a function that translates expressions such as
plus(v(10), mult(v(17), v(10)))
into machine code such as
(: load(r(0), l(10)),
   load(r(1), l(17)),
   load(r(2), l(10)),
   mult(r(1), r(2)),
   add(r(0), r(1))    :)    .
The compiler is constructive so that PVS ground evaluator can actually be used to generate the above machine code from the form:
compile(plus(v(10), mult(v(17), v(10))))    .
The compiler is proved correct, meaning that evaluating the source expression or the object code in the same environment will always produce the same value (in register r(0) for the object code). More precisely:
compiler_correctness: THEOREM
      (FORALL (me: machine.environment, ee: expressions.environment,
               e: expression):
         equivalent?(me, ee)
           IMPLIES
         eval(compile(e))(me)(r(0)) = eval(e)(ee)) ;

Definitions and properties of permutations

We first define permutations as bijective functions from nat to nat. A subset S of nat fullset is a support of a permutation s if s does not change naturals except maybe for those belonging to S. By extension, we say that permutation s admits the natural p for support if the interval [0, p[ is a support of s.

We then define a "permute?" relation among lists and nat permutations: permute?(l1, l2, s) holds if l2 is the result of applying s permutation to l1; permute?(l1, l2) holds if there is a permutation s such that permute?(l1, l2, s) holds: we show that it is an equivalence relation. The "permute?" relation actually has a slightly more general type:

permute?: [list[T], list[T], [nat -> nat] -> bool]


A functional version of the ternary permute? predicate can easily be obtained with type:

permute(l: list[T], s: (permutation?(length(l)))): {l_s: list[T] | permute?(l, l_s, s)}    ,
where the type "(permutation?(length(l)))" denotes permutations having "length(l)" for support. This is not yet provided, as this library is under construction.

Properties of well founded relations

In PVS, well founded relations are defined as relations such that every non empty set has a minimal element. Mathematicians tend to use a different definition: a relation is well founded iff there is no infinitely strictly decreasing sequence.

Strictly speaking, both definitions are not equivalent, since for PVS a well founded relation is necessarily irreflexive, which is not the case of the other definition. However, both definitions become equivalent if we replace "strictly decreasing" with "decreasing".

This library essentially establishes the following results:



© Copyright 2000 Paul Y Gloess