CS636 Week 7-14

WEEK 7 TAUTOLOGIES AND CONTRADICTIONS

Some propositions P(p, q, . . .) contain only T in their evaluation or, in other words, they are true for any truth values of their variables. Such propositions are called tautologies. Analogously, a proposition P(p, q, . . .) is called a contradiction if it contains only F in its evaluation or, in other words, if it is false for any truth values of its variables.

ARGUMENTS

An argument is an assertion that a given set of propositions P1, P2,...,Pn, yields another proposition Q. An argument provides support or evidence in favor of one of the others. An argument P1, P2, ..., Pn Ͱ Q is said to be valid if Q is TRUE whenever all the premises P1, P2,...,Pn are true. Eg: valid argument p, p → q Ͱ q

•  Now the propositions P1, P2, . . . , Pn are true simultaneously if and only if the proposition P1 ∧ P2 ∧ . . . Pn is true.
•  Thus the argument P1, P2, . . . , Pn Ͱ Q is valid if and only if Q is true whenever P1 ∧ P2 ∧ . . . ∧ Pn is true, or, equivalently, if the proposition (P1 ∧ P2 ∧ . . . ∧ Pn) → Q is a tautology.
•  Lets determine the validity of the following argument:
•  p → q, ¬ q Ͱ ¬p.

An argument which is not valid is called fallacy. Eg: fallacy argument p → q, q Ͱ p Show that the following argument is a fallacy: p → q, ¬p Ͱ ¬q.

THREE-VALUED LOGIC

Classical logic assumes that all expressions evaluate to TRUE or FALSE. In reality, this is not always the case when evaluating an expression, because sometimes an expression can be undefined For example, the expression 0/0. Undefined terms are very common in programming situations – for example, when a variable is first declared and has not yet been assigned a value. In this system of logic a proposition could have the value TRUE, FALSE or UNDEFINED.

AND Operator OR Operator · IMPLICATION Operator Equivalence Operator · Exclusive OR Operator Negation Operator · Predicate Logic

•  One of the limitations with the propositional logic is that, while it allows us to argue about individual values, it does not give us the ability to argue about sets of values.
•  A set is any well-defined, unordered, collection of objects. The set of whole numbers from 1 to 10 The set of the days of the week
•  In mathematics, we often represent a set elements by lower-case letters. For example:
•  A = {s, d, f, h, k}
•  B = {a, b, c, d, e, f}
•  The symbol ∈ means ‘is an element of’. Therefore the statement ‘d is an element of A’ is written: d ∈ A
•  For the purpose of reasoning about sets of values, a more powerful tool than the propositional logic has been devised, namely the predicate logic.
•  A predicate is a truth-valued expression containing free variables. These allow the expression to be evaluated by giving different values to the variables.
•  Once the variables are evaluated they are said to be bound.

Example of predicates

•  Predicates can be named with either a single letter, or with a word that expresses the meaning of the predicate; the variables are placed in brackets after the name.
•  This is made clear in the following examples:  C(x): x is a cat  Studies(x,y): x studies y  Prime(n): n is a prime number
•  A statement such as C(x) can be read C of x.
•  Predicates such as those above do not yet have a value – they only have a value when the variables themselves are given a value.

Binding variables

Predicates do not yet have a value – they only have a value when the variables themselves are given a value. Two ways: Substitution Quantification

Binding (Substitution)

For example, using the previous three predicates: C(Simba): Simba is a cat Studies(Ali, physics): Ali studies physics Prime(3): 3 is a prime number The above expressions now have a value of TRUE or FALSE.

Binding (Quantification)

A quantifier is a mechanism for specifying an expression about a set of values. There are three quantifiers that we can use, each with its own symbol: Universal Quantifier Existential Quantifier Unique Existential Quantifier

Quantification

 The universal quantifier ∀:  This quantifier enables a predicate to make a statement about all the elements in a particular set. For example, if M(x) is the predicate x chases mice, we could write:  ∀x ∈ Cats ● M(x)  This reads For all the x which are members of the set Cats, x chases mice, or, more simply, All cats chase mice.  – The existential quantifier ∃  In this case, a statement is made about whether or not at least one element of a set meets a particular criterion.  For example, if, as above, P(n) is the predicate n is a prime number, then we could write:  ∃n ∈ ℕ ● P(n)  This reads There exists an n in the set of natural numbers such that n is a prime number, or, put another way, There exists at least one prime number in the set of natural numbers.  –The unique existential quantifier ∃!  This quantifier modifies a predicate to make a statement about whether or not precisely one element of a set meets a particular criterion.  For example, if G(x) is the predicate x is green, we could write  ∃!x ∈ Cats ● G(x)  This would mean There is one and only one cat that is green.

WEEK 8

Intoduction to Specification in VDM-SL

At the end of this chapter you should be able to: write a formal specification of a system in VDM-SL correlate the components of a UML class diagram with those of a VDM specification declare constants and specify functions to enhance the specification explain the use of a state invariant to place a global constraint on the system explain the purpose of the nil value in VDM

The Case Study: Requirements Analysis

The example we will use throughout this chapter will be that of an incubator, the temperature of which needs to be carefully controlled and monitored in order to provide the correct conditions for a particular biological experiment to be undertaken. We will specify the software needed to monitor and control the incubator temperature. In developing any software system the first stage in the process involves an analysis of the system and an initial statement of the requirements. It is very important, in any requirements definition, to be clear about the system boundaries, and we should make it clear here that in this initial version, control of the hardware lies outside of our system. In other words, for the time being we will be specifying a system that simply monitors the temperature of the incubator.

The Incubator - Case Study

The hardware increments or decrements the temperature of the incubator in response to instructions (from someone or something outside of our system), and each time a change of one degree has been achieved, the software is informed of the change, which it duly records. However, safety requirements dictate that the temperature of the incubator must never be allowed to rise above 10 degree celsius, nor fall below -10 degree celsius.

The UML Specification

In the simple system described in the previous slide, we can identify a single class, IncubatorMonitor. We have identified one attribute and three methods. The single attribute records the temperature of the system and will be of type integer. With regard to the methods, the first two do not involve any input or output (since they merely record an increase or decrease of one degree). The final method reads the value of the temperature, and therefore will output an integer.

Specifying the State

The first thing we will consider for our formal specification is what is known as the state of the system. In VDM-SL the state refers to the permanent data that must be stored by the system, and which can be accessed by means of operations.

Intrinsic types available in VDM-SL

N: natural numbers (positive whole numbers) N1: natural numbers excluding zero Z: integers (positive and negative whole numbers) R: real numbers (positive and negative numbers that can include a fractional part) B: boolean values (TRUE or FALSE) Char: the set of alphanumeric characters

Specifying the Operations

We need to specify a number of operations that the system should be able to perform and by which means the data (that is the state) can be accessed. In VDM we tend to use the word operation, whereas in most objectoriented texts you will tend to see the word method. In VDM, operations by definition access the state in some way, either by reading or writing the data, or both.

Operations in VDM-SL

In VDM-SL an operation consists of four sections: the operation header the external clause the precondition the postcondition We need to consider: an operation that records an increment in the temperature; an operation that records a decrement; and one that simply reads the value of the temperature.

Declaring Constants

As with many programming languages, it is possible in VDM-SL to specify constants.