Get premium membership and access revision papers, questions with answers as well as video lessons.
Bct2313:Formal Software Specifications Question Paper
Bct2313:Formal Software Specifications
Course:Computer Technology
Institution: Meru University Of Science And Technology question papers
Exam Year:2013
1
QUESTION ONE – 30 MARKS
a. What are formal methods? Outline four reasons of using specification in software development.
(6 Marks)
b. By use of suitable symbols, explain the following inference rules: (6 Marks)
i. Modus pones
ii. And - elimination
c. Write the predicate for each of the following statements. (4 Marks)
- If Jane is a math major or Jane is a computer science major, then Jane will take math 100
- If it is raining, then I am carrying an umbrella.
d. Consider the following informal specifications:
The function sum should take as its argument a list of numbers. If the numbers are all positive, it should
return their sum. The function BinarySearch should take as its first argument a sorted list of integers (in
ascending order), and as its second argument a single interger; it should return true if the second
argument is found in the list. The student class contains a list of modules studied by the student (as
interger IDs). These are sorted in descending order. The method is studying should use the function
BinarySearch to find a particular ID in the list.
Find 3 errors in the above informal specification that could be caught by the use of formal methods.
What kind of error is each? (6 Marks)
2
e. Formalize the above circuit in propositional logic such that any satisfying interpretation represents a
feasible system state. (6 Marks)
f. What are hidden sorts used for in formal methods. (2 Marks)
QUESTION TWO – 20 MARKS
a. What is specification? Where does it fit into the software lifecycle? (4 Marks)
b. Let people be the set of all possible persons and subjects the set of all possible subjects. A specification
for a university has a state schema:
i. For the class university, specify an operation schema newStudent such that a person becomes a
student. (4 Marks)
ii. An operation schema StudentLeaves such that a person, not enrolled in any subject, ceases to be a
student. (4 Marks)
iii. An operation schema personSubjects which outputs the set of subjects in which the person is
enrolled. (4 Marks)
c. Distinguish between procedural abstraction and data abstraction as used in software design. (4 Marks)
QUESTION THREE – 20 MARKS
a. Explain the term refinement in the domain of formal methods. (4 Marks)
b. Determine if the following propositions is valid using truth tables. (6 Marks)
((P?H) ? ¬ H) P
c. Explain with suitable example the principle of operation of heap sort. (4 Marks)
d. Explain the steps in the abstract model specifications. (6 Marks)
3
QUESTION FOUR – 20 MARKS
a. Represent the following statements as propositions using ‘well-formed formula’ (wff): (3Marks)
- Someone is a sister of another if that person is a female and both have same father and
same mother
b. Describe the process of mapping the transaction to the analysis model. (6 Marks)
c. i. Distinguish between push and pop as used in stack. (2 Marks)
ii. Write an algorithm that could implement a stack. (4 Marks)
d. Describe the user interface design process. (5 Marks)
QUESTION FIVE – 20 MARKS
a. Consider the following propositions:
? x: ?y: cat(x) ? fish(y) likes_to_eat (x,y)
Write the proposition for this statement. (4 Marks)
b. Describe each of the following architectural design techniques. (4 Marks)
i. Factoring
ii. Vertical portioning
c. i. What is a graph, give two practical examples of graph applications? (4 Marks)
ii. Consider the following pairs of nodes:
13, 21, 16, 24, 31, 19, 68, 65, 26, 32
Represent the pairs of nodes using binary Min Heap. (4 Marks)
d. Represent the specification of the following scenario in high order logic. (4 Marks)
The state space of a library system represents a member and book. A book is either on the shelf or
loaned to a member. (4 Marks)
More Question Papers
Popular Exams
Return to Question Papers