Formal Methods in Software Engineering

Formal Methods in Software Engineering
Lecture 03
Recapping…..
 What is Logic? In computer science, the aim of the logic is to
develop a language that models a situation, in which, it can reason
formally to realize the desired objective.
 What is Reasoning? Reasoning is a process of using existing
knowledge or observations to make predictions or draw conclusions.
 Due to basic techniques of logical formalisms, formal methods were
born.
 Formal methods are used in the industry with their specification
languages, theorem proving, and model checking
What is Propositional Logic?
 Propositional Logic (PL) is a formal language, which is often used in

behavior analysis of computing systems.
 PL is based on mathematical modelling that can be used to perform

reasoning about the truthfulness or falsehood of logical expressions.
 The core idea of propositional logic is to develop a language to

model the situation in a manner where reasoning can be performed
formally to express properties of a system.
Why Propositional Logic?
 Most of modern formal specifications and proofs are

performed with the use of propositional logic and predicate
logic.
 Propositional logic is a useful tool for modelling and reasoning

in diverse application domains, especially in digital circuits.
Atomic proposition
 Propositional logic is based on propositions and propositional

formulas, which are written in a propositional language.
 Proposition: A declarative sentence that may either be true or

false.
 Propositions / sentences express the atomic concepts about the

world.
 Propositional Variables: Propositions / sentences are represented by

propositional variables such p, q, r, … For example; p: The sun is shining
Atomic proposition
 Examples:
 The sun is shining ---- True or False
 It is a fall season ---- True or False
 Islamabad is the capital of Pakistan ---- True
 0 + 1 = 1---- True
 0 + 1 = 2---- False
 Example of non-propositions
 Pease listen lecture carefully!
 What is your name?
 x+1=2
Compound Proposition
 Compound proposition are constructed from simple proposition

 Two or more propositions are joined using logical connectives
 In formal methods, the natural language is scan for propositions.
Each proposition (either True or false) will be translated into an
expression usually joined using operators.
Translating English sentences to
statement in propositional logic
 Identify atomic propositions and represent using propositional variables.
 Determine appropriate logical connectives
Example;
 “If time is 8:00-9:30 am and room CS003 is occupied, then Formal method class
is going on.”
 p: time is 8:00-9:30 am
 q: room CS003 is occupied.
 r: Formal method class is going on.
If p and q then r.  p^q  r

Precedence of logical Connectives in
PL
Negation
 Proposition: A = It is raining.
 Possible value: true or false therefore in a truth table.
(A) It is raining
F
 Proposition: ⌐A = It is not raining or Not (It is raining).
 Possible value: true or false therefore in a truth table.
A Results (⌐A)
T F
F T
Disjunction
 The disjunction of propositions p and q is denoted by p ∨ q
p q pvq
T T T
T F T
F T T
F F F
Disjunction Example
 (P v Q) v R
Conjunction
 The conjunction of propositions p and q is denoted by p ^ q
p q p^q
T T T
T F F
F T F
F F F
Conjunction Example
 P v (Q ^ R)
Implication
 If p and q are propositions, then p → q is a conditional

statement or implication which is read as “if p, then q” and
has this truth table:
p q P→q
T T T
T F F
F T T
F F T
Implication
 In p → q, p is the hypothesis (antecedent) and q is the conclusion (or

consequence)
 Implication can be expressed by disjunction and negation:

p → q ≡ ¬p ∨ q
 In p → q there does not need to be any connection between the

antecedent or the consequent. The meaning depends only on the truth
values of p and q.
Implication Example
 p → (q → r)
Bi-implication / equivalence
 If p and q are propositions, then bi-implication proposition

p ↔ q has this truth table
p q P↔ q
T T T
T F F
F T F
F F T
 p ↔ q also reads as:

 p if and only if q
 p iff q.
Equivalence Example
 (p → q) ^ (q → p)
Tautology and Contradiction
 Tautology
 if it is always true.
 When all results in the truth table are true
 Example: p ∨ ¬p.
 Contradiction /Un-satisfiability
 if it always false.
 When all results in the truth table are false
 Example: p ∧ ¬p.
Satisfiability
 A formula is satisfiable if it holds under some or all assignments,

which means the truth values of conclusion, some values are true
and some values are false.
 It may be possible that all values are true.
p q p→q p^(p → q) p^(p → q) →q
T T
T F
F T
F F
Laws in Propositional Logic
 Assignment Due Date: 13-March-2019 Time 8:30

Formal Methods in Software Engineering

Uploaded by

Copyright:

Available Formats

Formal Methods in Software Engineering

Uploaded by

Document Information

Original Description:

Original Title

Copyright

Available Formats

Share this document

Share or Embed Document

Sharing Options

Did you find this document useful?

Is this content inappropriate?

Copyright:

Available Formats

Formal Methods in Software Engineering

Uploaded by

Copyright:

Available Formats

Formal Methods in Software Engineering

 Propositional Logic (PL) is a formal language, which is often used in

 PL is based on mathematical modelling that can be used to perform

 The core idea of propositional logic is to develop a language to

 Most of modern formal specifications and proofs are

 Propositional logic is a useful tool for modelling and reasoning

 Propositional logic is based on propositions and propositional

 Proposition: A declarative sentence that may either be true or

 Propositions / sentences express the atomic concepts about the

 Propositional Variables: Propositions / sentences are represented by

 Compound proposition are constructed from simple proposition

If p and q then r.  p^q  r

 The disjunction of propositions p and q is denoted by p ∨ q

 The conjunction of propositions p and q is denoted by p ^ q

 If p and q are propositions, then p → q is a conditional

 In p → q, p is the hypothesis (antecedent) and q is the conclusion (or

 Implication can be expressed by disjunction and negation:

 In p → q there does not need to be any connection between the

 If p and q are propositions, then bi-implication proposition

 p ↔ q also reads as:

 A formula is satisfiable if it holds under some or all assignments,

p q p→q p^(p → q) p^(p → q) →q

 Assignment Due Date: 13-March-2019 Time 8:30

You might also like