University:
Anglia Ruskin University
Course:
BSE1300 | Software Engineering
Academic year:

2021
Views:

223

Pages:

2
Author:

Sharookh N.

Axiomatic Specification Software Engineering ___ Notes Axiomatic specification of a system presents a set of rules that govern a system by specifying pre and post conditions that describe the behavior and effectiveness of the system as axioms in first-order logic. This is done by using the axiom of induction.The pre-conditions delineate the states required to allow the successful invocation of an operation. In other words, pre-conditions capture the necessary conditions for proper performance of a function in the absence of the post-conditions. The post-conditions on the other hand are constraints that should be met after the function finishes its theatrical act in order to consider that the function was carried out without any trouble. They are constraints placed upon the results that are supposed to be the outcomes of the function completion. Now the explanation below gives the patterns for systematic development of axiomatic specification of a function: ● Determine the domain of inputs at which the function must perform the relevant operations.Also elaborate on any other prerequisites on the inputs, then there are the conditions which are specified asa predicate. ● State a predicate explaining what needs to be the condition of the output of the function so that,it has performed correctly. ● Examine what happens to the inputs of the function after it has executed. There are cases wherepure mathematical functions are concerned, the inputs do not get changed and hence that ends up not being a valid claim with pure functions in particular. ● Capturing all of the discussed conditions then define and enforce them as the pre and post conditions respectively of the function. Example1: - Describe the conditions of a function that would deal with real arguments; it must follow that the function results in its foremost argument being halved, if it is not more than 100, and in finding of the product when greater than 100. Example2: Evidently identify a function named search that takes an integer array and an integer key value as its parameters and outputs the index in the array where the key value is observed. To alter the definition of the argument X used in a function call due to a function activity, we denote this as X’ once the function calling is over.