Adam Koprowski - Introduction to PVS (Adam Koprowski - Introduction to PVS.pdf)
Описание файла
PDF-файл из архива "Adam Koprowski - Introduction to PVS.pdf", который расположен в категории "". Всё это находится в предмете "практика" из 9 семестр (1 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст из PDF
Introduction to PVSProving with computer assistanceAdam Koprowski22 May 2008A.Koprowski@tue.nlHG 6.78Adam KoprowskiIntroduction to PVSPVSPVSPVS: Prototype Verification Systemhttp://pvs.csl.sri.comSpecification and verification system consisting of:formal specification language,model checker,theorem prover,documentation, administrative tools etc.Adam KoprowskiIntroduction to PVSPVS: applicationsBoth academic and industrial:verification of Javacard applets (LOOPtool, Nijmegen),hardware verification (microprocessors, ATM switches),protocol specification and verification,formal mathematics,safety-critical systems (NASA)and many more:http://pvs.csl.sri.com/users.shtmlAdam KoprowskiIntroduction to PVSPVS: practical aspectsDownloadable from http://pvs.csl.sri.com(Windows not supported!).Last version: 4.1.Available on svstud (via Exceed).Emacs interface.Adam KoprowskiIntroduction to PVSPVS: the system & its logicPVS: the systemImplemented in LISP (more than 50.000 lines).Theories written and edited in text files (*.pvs).Proofs created interactively and saved as LISPdata-structure (*.prf).PVS: the logicBased on extensions to typed λ-calculusand classical, typed higher-order logic.Extensions allow for subset types.Reliability: unlike Coq, PVS does not have a small kernel (deBruijn principle)=⇒ in previous version, 0 = 1 has been provenAdam KoprowskiIntroduction to PVSPVS typesType variables: T : Type, T : Type+.Base types: bool, nat, real.Abstract data-types: Stack, List, Tree.Function types: [int, nat−> bool].Enumeration types: {red, green, blue}.Tuple types: [A, B].Dependent record types: [# a : A, b : B(b) #].Subset types: {i : nat | i > 1}.Adam KoprowskiIntroduction to PVSPVS expressionsBasic expressions:TRUE : bool0, 23 + 5, 17 ∗ 10 : intFunction abstraction and application:(LAMBDA (i, j : nat) : i + j) : [nat, nat -> nat]f(i, j)Logic:AND, OR, NOT, IMPLIES, IFF, =, / =, FORALL, EXISTSConditionals:IF c THEN e1 ELSE e2 ENDIFRecords:point WITH [‘x := 24]Subtypes:Interval(m, n : int) : TYPE = {i : int | m <= i <= n}/ : [int, {n : int | n/ = 0} -> int]Adam KoprowskiIntroduction to PVSPVS recursive definitionssum(n : nat) : RECURSIVE nat =(IF n = 0 THEN 0 ELSE n + sum(n − 1) ENDIF )MEASURE nThis recursive definition generates two type checkingconditions:for type-consistency: IF n /= 0 THEN n − 1 >= 0for termination: IF n /= 0 THEN n − 1 < nSuch conditions are called TCCs (Type Checking Conditions).They:are generated for recursive definitions and subtypes andmost of them can be automatically discarded by PVS.Type-checking in PVS is not decidable!Adam KoprowskiIntroduction to PVSPVS theoriesPVS developments are organized into theories.Theories consist of definitions, declarations, axioms andlemmas.Theories can be parameterized.Prelude contains a (large) number of predefined theories.wf _induction [T : TYPE, <: (well_founded?[T ])] : THEORYBEGINwf _induction : LEMMA .
. .END wf _inductionAdam KoprowskiIntroduction to PVSPVS sequentsPVS proof obligations are presented as sequents:{-1} A{-2} B|----------[1]S[2]TThe sequent stands for: A ∧ B =⇒ S ∨ T with:negatively numbered ancedents/assumptions above theline,positively numbered consequents/goals below the line.PVS maintains a proof tree of such sequents.Note that the following two sequents are equivalent!{-1} A|----------...and...|---------[1] NOT AAdam KoprowskiIntroduction to PVSBasic tactics(undo) - undo the last step in the proof.(quit) - quit the current proof.(postpone) - go to the next proof obligation.(help), (help postpone) - get help.Adam KoprowskiIntroduction to PVSComparison of tacticsCoqintro, introsapplyunfoldsimplinductionauto, tautorewriteUndoPVS(flatten), (skolem)(lemma), (use)(expand)(beta), (simplify)(induct), (induction-and-simplify)(grind), (prop), (assert)(rewrite), (replace)(undo)Adam KoprowskiIntroduction to PVSflatten{-1} A AND B|------------...(flatten -1)...|----------[1] A OR B(flatten)...|----------[1] A => B(flatten)Adam Koprowski{-1} A{-2} B|------...|-----[1] A[2] B{-1} A|------[1] BIntroduction to PVSsplit...|-----------[1] A AND B{-1} A OR B|-----------...(split 1)|------ and |-----[1] A[1] B(split -1)Adam Koprowski{-1} A{-1} B|------- and |------......Introduction to PVSTactics for propositional logic(flatten [fnum]) - flatten assumptions (A AND B)and goals (A OR B).(split [fnum]) - split proof obligations based onassumptions (A OR B) or goals (A AND B).(case "formula") - case distinction on the formula, ex.(case "x > 0").(lift-if [fnum]) - lift branching to the top level of theformula, i.e.: f(IF b THEN e1 ELSE e2 ENDIF)becomes: IF b THEN f(e1) ELSE f(e2) ENDIF.(prop) - automatic strategy for propositional logic.Adam KoprowskiIntroduction to PVSskolem...|----------------------- (skolem! 1) |----------[1] FORALL (x:A) : P(x)[1] P(x!1){1} EXISTS (x:A) : P(x)P(x)|----------------------- (skolem -1 "x") |----......Notes:(skosimp) does (skolem!) and (flatten).(skosimp*) does that repeatedly.Adam KoprowskiIntroduction to PVSinst...|---------------------- (inst 1 "w") |-------[1] EXISTS (x:A): P(x)[1] P(w){-1} FORALL (x:A): P(x){-1} P(w)|----------------------- (inst -1 "w") |--------......Adam KoprowskiIntroduction to PVSTactic for predicate logic(skolem! [fnum]) - introduce skolem constants forgoals FORALL(x) P or assumptions EXISTS(x) P.(skolem [fnum] "name_1" ...
"name_N") allows you to choose the name(s) for those constants.(inst [fnum] "exp_1" ... "exp_N") - instantiateassumptions FORALL(x) P or provides witness for goalEXISTS(x) P.(inst? [fnum]) - PVS will guess the expression;works only for very simple cases.Adam KoprowskiIntroduction to PVSTactics for equational reasoning(expand "name" [fnum] [n]) - expand n’thoccurrence of name in formulas fnum (default: alloccurrences in all formulas)(replace fnum [fnums] LR/RL) use assumptions ofthe form l = r to replace l by r in formulas fnums.(assert) - built-in decision procedure for equality.Adam KoprowskiIntroduction to PVSMore tacticsUsing lemmas:(lemma "name") - add lemma name as an assumption.(rewrite "name" [fnums] RL) - like (replace) butusing a lemma instead of an assumption.Induction:(induct "n") - perform induction on variable n.
Thegoal should be of the form FORALL (..., n:nat,...): P(n).(induct-and-simplify "n") - ditto, but performssimplifications after applying induction.Automation:(prop) - decision procedure for propositional logic.(assert) - decision procedure for equality logic.(grind) - a powerful “catch-all” automation strategy(note: if it does not succeed completely it can transformthe goal to unprovable/unreadable form).Adam KoprowskiIntroduction to PVSPVS demoPVS demoAcknowledgments to Erik Poll.This PVS introduction (and the demo file) are based on hisone-day introduction course given in Eindhoven during IPAdays.http://www.cs.ru.nl/~erikpoll/Teaching/PVS/index.htmlAdam KoprowskiIntroduction to PVS.
