Formal Methods in software development
This content is about Formal Methods in Software Development for the academic year 2017/2018 under the guidance of Prof. Anna Labella. It delves into the principles and practices of using formal methods in software development processes to enhance quality and reliability.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Formal Methods in software development a.y. 2017/2018 Prof. Anna Labella 16/02/2025 1
The need of formal declarative sentences cfr. M. Huth M. Ryan ch.1 Logic in computer science Modelling and reasoning about systems 2 16/02/2025
Composing sentences: connectives Sentences are expressions that assume truth values Inductive definition of complex sentences via connectives 3 16/02/2025
Examples of sentences and of connectives Mary wants to go to the picnic Today sun is shining . Sun is shining and Mary is going to the picnic If it is raining Mary gets wet If it is raining and Mary has an umbrella, then Mary does not get wet 4 16/02/2025
Natural deduction calculus1 Propositional variables p, q, r .. Connectives Intuitive meaning: p is true iff p is not true p q is true iff p and q are both true p q is true iff one between p and q is true p q is true iff, supposing p true, q is true 5 16/02/2025
Natural deduction calculus1 6 16/02/2025
Natural deduction calculus 2 Sequents 1, 2, 3, .. A sequent is valid if we can prove it For this reason we introduce proof rules 7 16/02/2025
Natural deduction calculus 2 What is a proof: A proof is a finite sequence of elementary steps given by proof rules beginning with the left part of the sequent and ending with the right part 8 16/02/2025
Natural deduction calculus 3 Proof rules involving conjunction i. e1 e2. 9 16/02/2025
Exercises Prove p q, r p r p q q p (p q) r p (q r ) 10 16/02/2025
Natural deduction calculus 4 Proof rules involving double negation e i 11 16/02/2025
Exercise Prove (p q), r p r 12 16/02/2025
Natural deduction calculus 5 Modus Ponens e 13 16/02/2025
Natural deduction calculus 6 Modus Tollens (derived rule) MT 14 16/02/2025
Exercises Prove p q, (p q) r r p, p (p q) q q (p r), r , q p 15 16/02/2025
Natural deduction calculus 7 Implies introduction . . _______ i 16 16/02/2025
Natural deduction calculus 8 Use of assumptions 1. p q 2. q 3. p 4. q p premise assumption MT i (2,3) p q |_ q p (p q), q |_ p 17 16/02/2025
Exercise Prove |_ (q r) (( q p) (p r)) 18 16/02/2025
Natural deduction calculus 9 Metatheorem 1, 2, 3, .. Is equivalent to ( 1 ( 2 ( 3 .. ))) Proof by induction 19 16/02/2025
Natural deduction calculus 10 Rules involving disjunction i1 i2 20 16/02/2025
Natural deduction calculus 11 Introducing disjunction ___________________ e 21 16/02/2025
Exercises Prove p q q p (p q) r p (q r ) p (q p ) p q q p The Copy rule 22 16/02/2025
Natural deduction 12 About negation and e . . _______ i e 23 16/02/2025
Natural deduction calculus 13 Derived rules MT __________ LEM _______ RAA i 24 16/02/2025
Natural deduction calculus 14 Derived rules MT 25 16/02/2025
Natural deduction calculus 15 Derived rules __________ LEM 26 16/02/2025
Natural deduction calculus 16 Derived rules i 27 16/02/2025
Natural deduction calculus 17 Derived rules i 28 16/02/2025
29 16/02/2025
Natural deduction calculus 18 Provably equivalent formulas and , if we can prove both |_ and |_ 30 16/02/2025
Natural deduction calculus 19 Important remark (or metatheorem): The proof is obtained from the formula to be proved Hence it is automatic 31 16/02/2025
Exercises 32 16/02/2025
Exercises 33 16/02/2025
