1FORMAL SPECIFICATION A formal software specification is a statement expressed in a language whose vocabulary, syntax, and semantics are formally defined. The need for a formal semantic definition means that the specification languages cannot be based on natural language; it must be based on mathematics.2The advantages of a formal language are: • The development of a formal specification provides insights and understanding of the software requirements and the software design. • Given a formal system specification and a complete formal programming language definition, it may be possible to prove that a program conforms to its specifications. • Formal specification may be automatically processed. Software tools can be built to assist with their development, understanding, and debugging.3 • Depending on the formal specification language being used, it may be possible to animate a formal system specification to provide a prototype system. • Formal specifications are mathematical entities and may be studied and analyzed using mathematical methods. • Formal specifications may be used as a guide to the tester of a component in identifying appropriate test cases.4Formal specifications sometimes are not used because: • Software management is conservative and unwilling to adopt new techniques whose payoff is not immediately obvious. • Most software engineers have not been trained in formal specification techniques. • Some classes of systems are difficult to specify using existing specification techniques. Interactive and interrupt driven systems might be examples.5Relational and State-Oriented Notations Relational notations are used based on the concept of entities and attributes. Entities are elements in a system; the names are chosen to denote the nature of the elements (e.g., stacks, queues). Attributes are specified by applying functions and relations to the named entities. Attributes specify permitted operations on entities, relationships among entities, and data flow between entities.6Relational notations include implicit equations, recurrence relations, and algebraic axioms. State-oriented specifications use the current state of the system and the current stimuli presented to the system to show the next state of the system. The execution history by which the current state was attained does not influence the next state; it is dependent only on the current state and the current stimuli.7State-oriented notations include decision tables, event tables, transition tables, and finite-state tables.8SPECIFICATION PRINCIPLES Principle 1: Separate functionality from implementation. A specification is a statement of what is desired, not how it is to be realized. Specifications can take two general forms. The first form is that of mathematical functions: Given some set of inputs, produce a particular set of outputs. The general form of such specifications is find [a/the/all] result such that P(input), where P represents an arbitrary predicate. In such specifications, the result to be obtained has been entirely expressed in a “what”, rather than9a “how” form, mainly because the result is a mathematical function of the input (the operation has well-defined starting and stopping points) and is unaffected by any surrounding environment.10Principle 2: A process-oriented systems specification language is sometimes required. If the environment is dynamic and its changes affect the behavior of some entity interacting with that environment (as in an embedded computer system), its behavior cannot be expressed as a mathematical function of its input. Rather a process-oriented description must be employed, in which the “what” specification is achieved by specifying a model of the desired behavior in terms of functional responses to various stimuli from the environment.11 Principle 3: The specification must provide the implementor all of the information he/she needs to complete the program, and no more. In particular, no information about the structure of the calling program should be conveyed. Principle 4: The specification should be sufficiently formal that it can conceivably be tested for consistency, correctness, and other desirable properties.12Principle 5: The specification should discuss the program in terms normally used by the user and implementor alike.13SOME SPECIFICATION TECHNIQUES 1. Implicit Equations Specify computation of square root of a number between 0 and some maximum value Y to a tolerance E. (0<=X<=Y){ABS_VALUE[(WHAT(X))2-X]}<=E 2. Recurrence Relation14Good for recursive computations. Example, Fibonacci numbers 0, 1, 1, 2, 3, 5, 8,... FI(0) = 0, FI(1) = 1, FI(n) = FI(n-1) + FI(n-2),n>=1. 3. Decision Tables Good for state-oriented specifications. Example, credit approval.15 CONDTION 1 2 3 4 Credit Limit is Satis. y n n n Pay exp. is favorable - y n n Special Clear. - - y n ACTION Approve order x x x Reject order x 4. Event Table16Specify action to be taken when events occur under different sets of conditions. f(M,E)=A, where M denotes the current set of operating conditions, E is the event of interest, and A is the action to be taken (two-dimension table). Example: EVENT MODE E13 E37 E45 Start-up A16 - A14; A32 Steady x A6, A2 (Start-up, E13) = A1617x means impossible - means no action required A14; A32 means A14 followed by A32 A6, A2 means A6 and A2 concurrently 5. Transition Table18 Used to specify changes in the state of a system as a function of driving forces. f(si,cj) = sk means if f is in state si with the condition cj then the next state is sk Menu-driven software systems normally are based on such tables.19 Example, RS flip-flop behavior. R S Q Qn 0 0 0 0 0 0 1 1 0 1 0 1 0 1 1 1 1 0 0 0 1 0 1 0 1 1 0 - 1 1 1 -2021AXIOMATIC SPECIFICATIONS Use a set of stateless functions; each function has a set of pre- and post-conditions. Pre- and post-conditions are predicates over the inputs and outputs of a function. A predicate is a Boolean expression which is true or false and whose variables are the parameters of the function being specified.22Some predicates are: 1. A>B and C>D 2. exists i, j, k in M...N: i2 =j2 + k2 3. for-all i in 1...10, exists j in 1...10: squares (i)=j223Stages of axiomatic specification of a function: 1. Establish the range of the input parameters over which the function is