PVS‎ > ‎

language

PVS language is the result of a strong interaction between types and expressions, with the general paradigm:


    expressiontype


A PVS theory is essentially a list of declarations or definitions of expressions or types, plus theorems. There are thus two dimensions in this language:


expression

constant | function | formula

type

declaration

c
: typeexpr

f(p1: typexpr1, ..., pn: typexprn): typexpr

t: TYPE

t: TYPE+

t: TYPE FROM typexpr

definition
 ctypeexpr
= expr

f(p1typexpr1, ..., pntypexprn): typexpr

= expr


t
: TYPE
typexpr
 theorem name: THEOREM

formula

 


Function declaration or definition is a cosmetic variant of constant declaration or definition: it does not add any expressive power.


PVS type language is so powerful, because of subtyping (by means of predicates) that type checking is undecidable: this is why PVS generates TCCs (Type Checking Conditions) that often require user interaction (to come up with proofs). Undecidability of type checking can be viewed as a bad and good thing:

  • bad: PVS type checker is like a compiler that would not be able to automatically compile a program;
  • good: TCC automatic generation help the user pinpoint specification flaws, and determine what needs to be proved;
  • bad & good: the user has great freedom of expression and can write incorrect specifications, but won't be able to prove them correct.

Predicate subtyping, combined with dependant types, allows the specification of functions by means of types.


LAMBDA, EXISTS, FORALL uniform syntax

  • (LAMBDA (x1typexpr1, ..., xntypexprn): expr) with cosmetic variant {x1typexpr1, ..., xntypexprexprwhen expr: bool
  • (EXISTS (x1typexpr1, ..., xntypexprn): exprwhen exprbool
  • (FORALL (x1typexpr1, ..., xntypexprn): exprwhen exprbool

More on PVS language

The presentation below has been converted from “PowerPoint” to “Google Slides” format: please note that the conversion is not perfect, wait for fixes. Go to bottom of the page for “ppt” or “pdf” versions.

PVS language - Slides


Ċ
Paul Y Gloess,
13 sept. 2013 à 05:07
ć
Paul Y Gloess,
13 sept. 2013 à 05:08
Comments