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
|
Library dump
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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>.
plus(v(10), mult(v(17), v(10)))into machine code such as
(: load(r(0), l(10)),The compiler is constructive so that PVS ground evaluator can actually be used to generate the above machine code from the form:
load(r(1), l(17)),
load(r(2), l(10)),
mult(r(1), r(2)),
add(r(0), r(1)) :) .
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)) ;
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.
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: