Adam Koprowski - Introduction to PVS (811095)

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

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.

Характеристики

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов книги