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.
