Prototypverifieringssystem
Prototype Verification System ( PVS ) är ett specifikationsspråk integrerat med stödverktyg och en automatiserad teoremprovare , utvecklad vid Computer Science Laboratory of SRI International i Menlo Park, Kalifornien .
PVS är baserat på en kärna som består av en förlängning av kyrkans teori om typer med beroende typer , och är i grunden en klassisk typad logik av högre ordning. Bastyperna inkluderar otolkade typer som kan introduceras av användaren, och inbyggda typer som booleaner, heltal, reella och ordningstal. Typkonstruktörer inkluderar funktioner, uppsättningar, tupler, poster, uppräkningar och abstrakta datatyper. Predikatundertyper och beroendetyper kan användas för att införa begränsningar; dessa begränsade typer kan ådra sig beviskrav (kallade typkorrekthetsvillkor eller TCC) under typkontroll. PVS-specifikationer är organiserade i parametriserade teorier.
Systemet är implementerat i Common Lisp och släpps under GNU General Public License (GPL).
Se även
- Owre, Shankar och Rushby , 1992. PVS: A Prototype Verification System . Publicerad i CADE 11- konferensrapporten.
externa länkar
- PVS webbplats på SRI Internationals datavetenskapslaboratorium
- Sammanfattning av PVS av John Rushby i databasen Mechanized Reasoning av Michael Kohlhase och Carolyn Talcott