CSE510.assignments
The objective of assignments in the course is to illustrate how problems in
Software Engineering can be expressed and analyzed in a precise and unambiguous way.
The main vehicle here is the language of the propositional and predicate logic.
Traditionally, it was a paper-and-pencil way of expressing the programmer’s ideas
(models) about the program. That is, it was up to the reader of the model to
interpret it according to the laws of logic. Consequently, such an interpretation
was likely to suffer the unavoidable human limitations that too often lead to wrong
conclusions. Fortunately, nowadays there are tools that give the reader an immediate feedback
about the actual meaning of the model. One such tool is the IFAD VDM-SL Toolbox, whose
Syntax Checker, Type Checker and the Interpreter identify the real and potential problems
with the model.
The example below illustrates the use of VDM-SL Toolbox Interpreter.
Other assignments deal with sets, sequences, maps, relations, program specifications,
program call graphs (models of subprograms calling structure) and subprogram control
flow graphs (models of the execution order of subprogram statements).
Here is a sample of typical assignments.
Problem:
How to express the notion that array B is sorted array A?
First, in VDM-SL arrays are modeled by sequences. The following type Array
types
Array: seq of int;
is used in the following direct definition of the predicate IsSorted:
functions
IsSorted: Array * Array -> bool
"--" two dashes start a comment line
–- signature of the predicate: it takes two arrays as
-- arguments and returns a boolean value
IsSorted(A,B) ==
-–"==" stands for “defined as “
-- a direct definition
forall i in set {1,...,len A-1} & B(i) = B(i+1)
-– universal quantification: i ranges from 1 through size (length) of A - 1
pre len A = len B;
-- precondition, the arrays must have same length
Now, if we invoke the VDM-SL Interpreter and print (p) the value returned
by the predicate, we get the following:
IsSorted([4,2,1,5], [1,2,4,5]) = true
IsSorted([4,2,1,5], [1,4,5,2]) = false.
That’s good enough but the following test
IsSorted([4,2,2,7], [1,2,4,5])
also evaluates to true! The problem is that we did not require
that B be a permutation of A. To remedy this, we may define
IsSorted as follows
IsSorted(A,B) ==
(forall i in set {1,...,len A-1} & B(i) = B(i+1))
and
IsPermuted(A,B);
where the predicate IsPermuted(A,B) is true if and only if B
is a permutation of A. Of course, that predicate has to be
defined separately in a similar fashion.
|
