exam in discrete math
A1Homework_01
FrmlMeth.SoftwareEXLSGroupCASpringSemester2018CO-4262018-739AM.zipOverview2.html
This unit will cover how to use predicate calculus to represent program specifications.
Learning Objectives: Related course level objectives: 2 & 4
After completing the tasks of Module 9:
1. The student will be able to convert requirement specifications into predicate calculus.
2. The student will be able to use the existential and universal quantifiers to express requirements in predicate calculus.
3. The student will be able to translate predicates written in predicate calculus into natural language.
Tasks: To achieve the learning objectives of this module, you must do the following:
Read Chapter 4 and 5 in Ince.
Read the notes in the Week 9 folder.
Do the assignment(s) in the folder.
Participate in the discussion on Predicate Calculus in the Content Forum of the Discussion Tool.
Learning Objectives for this Week's Module: 1 - 3 will be assessed via discussions - both in the discussion tool, and answering questions from the lecture; 1 – 3 will also be assessed via the assignments.
Predicate CALCULUS.doc
PREDICATE CALCULUS
Propositional calculus is inadequate for expressing many system specifications.
There are two weaknesses of propositional calculus:
1. It is not possible to reason about classes of objects.
EX: “If all the valves are open, then at least one monitoring computer will be on-line.”
2. Propositional calculus manipulates objects which are not fine-grained enough to reason adequately about.
EX: “If one of the line voltages lies outside the range 110 to 220 degrees centigrade, then the line is malfunctioning.”
This sentence could be expressed as:
LineVolt110to200 => malfunction
But then you can’t reason about temperature values. What if you later learned that the LineVolt was 150? You couldn’t do anything with that fact – so just using the name to convey values or ranges is a big limitation.
To overcome limits of propositional calculus, we generalize a proposition in the following ways.
1) A proposition can be replaced by any expression which can be evaluated to either true or false. These expressions can contain:
· Identifiers which have integer values,
· Integer constants,
· Relational operators applied to integer variables and constants, and
· Arithmetic operators applied to integers.
EX: NewTemp > 10
OldMonitor > 10 => NewMonitor > 10
2.) A proposition can also include a construct which describes the relationship between two objects which can be variables or constants.
Relationships are written as:
name ( variable or constant, variable or constant)
and are similar to a Boolean function – they return a true or false value.
EX: IsConnected (computer1, computer7)
Returns true when computer1 is connected to computer7 and false otherwise.
The objects that can replace propositions in the propositional calculus are known as predicates.
The combined use of predicates and the operators of propositional calculus yields predicate calculus.
EX: “The reactor temperature lies between 0 and 10 degrees centigrade.”
Solution:
Temp >= 0 ^ temp <= 10
More Problems:
Convert the following to predicate calculus:
EX: “If the line voltage is active, then the line is malfunctioning.”
Solution:
LineVoltage (line, active) => LineState (line, malfunctioning)
EX: “Whenever the computer is brought off-line, the communications line is set to a high value of 5 volts”.
Solution:
ComputerState (computer, Offline) => ComVolt = 5
EX: “If the temperature of the main reactor is over 1000 degrees, then the monitoring computer is placed in an alarm state.”
Solution:
Temp (MainReactor, MainReacTemp) Λ MainReacTemp > 1000 =>
CompState (MonitoringComp, alarm)
Question: Why do we need to use MainReacTemp?
The above translates to:
“If the temperature of the main reactor is MainReacTemp and if the value of the MainReacTemp is greater than 1000 degrees then…
EX: Convert the following taken from a specification document into predicate calculus. Assume implication is not used.
“Only when the main computer is in a monitoring state will the subsidiary computer be in a monitoring state.”
Solution:
CompState (main, monitoring) (
CompState (subsid, monitoring)
hints_for_converting_into_predicate_calculus.docx
Hints for Converting into Predicate Calculus
1. Look for adjectives or modifying clauses. They indicate a relationship is needed.
Examples:
Invalid transaction
Main computer
Processor is on-line
Memory is occupied
2. Model these relationships as classes with attributes and instances.
Example:
Temp(MainReactor,MainReacTemp)
MainReactor
temp
has-a
MainReacTemp
Exercise 4.1.5
Question:
If more than six VDUs are currently active, and provided that the second processor is on-line, then a first-fit algorithm will be used for storage allocation.
Solution:
( state ( VDU , active ) ^ numberActiveVDU > 6 ) ^
( id ( processor , SecondProc ) ^ state ( processor , online ) ) =>
algoType ( algorithm , firstfit )
Partial models:
Processor
id
has-a
State
has-a
SecondProc
online
VDU
State
has-a
active
SET_SPECIFICATION.docx
SET SPECIFICATION
How do we specify the members of a set in a requirements specification? We could use the methods identified earlier in our Review of Set Theory such as enumeration. But for large sets, and in formal methods, the need for the set to be unambiguously defined requires a more formal technique.
The way of defining a set precisely is known as a comprehensive specification. It conforms to the general form:
{Signature |Predicate . Term}
We discussed this in chapter 4 under the name of set comprehension. The following is a review of that topic.
Set comprehension is a way to define a set by stating a property that distinguishes its members from other values of the type.
EX: {x : N | x < 5 . x2 }
Is the same set as: {0, 1, 4, 9, 16, 25}
Read: “The set formed from the natural numbers x such that x < 5 consisting of the squares of the x’s”
Set comprehension is a brief way of saying it.
Suppose D denotes some declarations,
P is a predicate constraining the values
E is an expression denoting a term, then:
{D | P . E}
is a set comprehension term and it denotes a set of values consisting of all values of term E for everything declared in D satisfying constraint P.
| Vertical bar is the constraint bar – it separates declarations from the constraint
. Heavy dot – separates the constraint from the term
Sometimes you can omit the constraint and the constraint bar:
{ x : N . x2 }
is the set of square natural numbers.
Chapter 5 ties in all of the concepts from the Set Theory review with all that we learned about predicate calculus.
You should be able to read Chapter 5 and solve the problems based on your cumulative knowledge.
SET COMPREHENSION.doc
SET COMPREHENSION
Set comprehension is a way to define a set by stating a property that distinguishes its members from other values of the type.
EX: {x : N | x < 5 . x2 }
Is the same set as: {0, 1, 4, 9, 16, 25}
Read: “The set formed from the natural numbers x such that x < 5 consisting of the squares of the x’s”
Set comprehension is a brief way of saying it.
Suppose D denotes some declarations,
P is a predicate constraining the values
E is an expression denoting a term, then:
{D | P . E}
is a set comprehension term and it denotes a set of values consisting of all values of term E for everything declared in D satisfying constraint P.
| Vertical bar is the constraint bar – it separates declarations from the constraint
. Heavy dot – separates the constraint from the term
Sometimes you can omit the constraint and the constraint bar:
{ x : N . x2 }
is the set of square natural numbers.
QUANTIFIERS
If x and y are integers, then the truth value of
x = y2
depends on the values of x and y. So x and y are the free variables of the predicate.
Existential quantifier : says “There exists” or “for some”
EX: y: Z . x = y2
Says “There exists an integer y such that x = y2 “
is always followed by a declaration, so it is followed by a heavy dot and a predicate being quantified.
There might be a constraint on the declaration and so the constraint bar may be used:
D | P . Q
EX: y : Z . x = y2
versus: existential quantification where the declaration is modified by a constraint:
n : N |n < 10 . n2 = 64
Says “There exists a natural number less than or equal to 10 whose square is 64”
Universal quantifier : says everything of a certain kind has a given property
EX: y : Z . y2 > x
Says “For all y that is an integer, y2 > x”
OR “every integer has a square that is greater than x”
Just like is always followed by a declaration, so it is followed by a heavy dot and a predicate being quantified.
There might be a constraint on the declaration and so the constraint bar may be used:
D | P . Q
EX with constraint bar:
n: N |n < 10 . n2 < 100
Says “For every natural number n < 10, n2 < 100”
Mixing Quantifiers : If a predicate begins with two quantifiers, one and onedon’t switch their order.
EX: x : Z .(y : Z . y > x )
Says “Given any integer we can always find one bigger than it” -- which is TRUE
BUT: y: Z . (x : Z . y > x )
Says “We can find an integer that is bigger than all the integers” -- which is FALSE
SET+COMPREHENSION+with+ExamplesLecture.doc
SET COMPREHENSION
Set comprehension is a way to define a set by stating a property that distinguishes its members from other values of the type.
EX: {x : N | x < 5 • x2 }
Is the same set as: {0, 1, 4, 9, 16, 25}
Read: “The set formed from the natural numbers x such that x < 5 consisting of the squares of the x’s”
Set comprehension is a brief way of saying it.
Suppose D denotes some declarations,
P is a predicate constraining the values
E is an expression denoting a term, then:
{D | P • E}
is a set comprehension term and it denotes a set of values consisting of all values of term E for everything declared in D satisfying constraint P.
| Vertical bar is the constraint bar – it separates declarations from the constraint
• Heavy dot – separates the constraint from the term
Sometimes you can omit the constraint and the constraint bar:
{ x : N • x2 }
is the set of square natural numbers.
QUANTIFIERS
Propositional calculus is unable to adequately express statements about the properties of classes of objects and to reason about them.
What we need is mathematical shorthand for expressing propositions that hold for a class of objects. We will use two operators known as the existential quantifier and the universal quantifier .
If x and y are integers, then the truth value of
x = y2
depends on the values of x and y. So x and y are the free variables of the predicate.
Existential quantifier : says “There exists” or “for some”
EX: y: Z • x = y2
Says “There exists an integer y such that x = y2 “
is always followed by a declaration, so it is followed by a heavy dot and a predicate being quantified.
There might be a constraint on the declaration and so the constraint bar may be used:
D | P • Q
EX: y : Z • x = y2
versus: existential quantification where the declaration is modified by a constraint:
n : N |n < 10 • n2 = 64
Says “There exists a natural number less than or equal to 10 whose square is 64”
Universal quantifier : says everything of a certain kind has a given property
EX: y : Z • y2 > x
Says “For all y that is an integer, y2 > x”
OR “every integer has a square that is greater than x”
Just like is always followed by a declaration, so it is followed by a heavy dot and a predicate being quantified.
There might be a constraint on the declaration and so the constraint bar may be used:
D | P • Q
EX: with constraint bar:
n: N |n < 10 • n2 < 100
Says “For every natural number n < 10, n2 < 100”
Mixing Quantifiers : If a predicate begins with two quantifiers, one and onedon’t switch their order.
EX: x : Z • (y : Z . y > x )
Says “Given any integer we can always find one bigger than it” -- which is TRUE
BUT: y: Z • (x : Z • y > x )
Says “We can find an integer that is bigger than all the integers” -- which is FALSE
An expression which is quantified is itself a predicate (i.e., has a truth value) and can be used in conjunction with other predicates.
Predicates can be formed from quantifiers and the standard propositional operators such as ^, V, ¬.
Examples:
Translate:
t: transactions • TransState (t, valid)
r: CurrentReactors; m: AllocatedMonitors • MonState (m, Functioning) ^ connected (r,m)
vdu: AllocatedVdus • VduState (vdu,on) => GlobalStatus (vdu, active)
Convert into predicate calculus:
One of the queues will always be in an active state.
queue: AvailableQueues • QueueState (queue, active)
One of the actuators will be functioning provided that the system ambient temperature is within safety limits and the main reactor is not in a warm-up state. The current safety limits are 10 to 100 degrees centigrade.
SOL:
AmbTemp 10 ^ AmbTemp < 100 ^
¬ ReactorState (main, Warmup) =>
a: acts • ActuatorState (a, functioning)
Translate:
n: 1..10 • n3 < 1000
valve: ExhaustValves • ValveStatus (valve,open) Ve ValveStatus (valve,closed)
p: ProgsInMemory • ProgState (p, suspended) => pr: processors • ProcessorState (pr, idle)
Possible solutions Ex.4.1.html
2.AcctNo > 100 ∧ Amount≥10 ∧ Amount ≤ 200 ⇒ ValidationState (transaction,valid)
4.OnlineStatus(reac,online)∧NumberOfreac ≤ 7
6.MemOccupPortion (mem,ocu)∧ ocu > 0.75 ⇒ NumofInteractiveUsers(system,uno)∧ uno ≤ 12
8.FieldLength (address,length) ∧ length > 10 ⇒ TransactionState(transaction,rejected)
Table of Contents.html
| Frml Meth. Software E XLS Group CA Spring Semester 2018 CO - Week 9
3. hints_for_converting_into_predicate_calculus 6. SET+COMPREHENSION+with+ExamplesLecture |
