Specifications

Subsection 1.3.5 Specifications

Sometimes we want to start with claims that we are determined to make true. We call these claims specifications. Specifications play a critical role in all kinds of design tasks, from computer software and hardware to the Internet to corporate databases.

Problem domain experts write specifications for software (and/or hardware) systems. Then other people (engineers with the necessary skills) build systems to meet those specifications. Disasters occur when the specifications are fuzzy or unclear. The use of a precise logical specification language can prevent such disasters. It can also make it possible to prove that a particular implementation does in fact meet the specifications.

So we’ll represent specifications as logical statements.

Software Specifications

Claim 1.3.4.

A University course scheduling program: No student is scheduled for back to back classes in buildings more than 2 blocks apart.

Claim 1.3.5.

A newsletter mailing program: Before the mailing labels are printed, the addresses are sorted by zip code.

Claim 1.3.6.

A loan underwriting program for a bank: Loans are issued only to people who have been customers of our bank for at least a year and whose credit score is at least 650.

Circuit Design Specifications

Hardware too is first specified, then designed and built.

Claim 1.3.7.

We might write this specification for a four-input, one-output circuit. It should compute:

NOT ((A AND B) OR NOT C) AND D)

Here’s a circuit that meets this specification:

Problems 1.3.10.

Consider the following procedure:

return(average(inputlist))

Now consider each of the following specifications. For each, indicate whether our procedure satisfies the specification.

(a)

Given a list of positive integers, return a positive no larger than the largest on the list.

Satisfies the specification
Doesn’t satisfy the specification

Answer.

i is correct.

Solution.

Explanation: The average of a list of numbers cannot be greater than the largest number in the list.

(b)

Given a list of positive integers, return some integer on the list.

Satisfies the specification
Doesn’t satisfy the specification

Answer.

ii is correct.

Solution.

Explanation: Suppose that the input list were [1, 7]. Our procedure will return 4, which isn’t on the list.

(c)

Given a list of positive integers, return some even integer on the list.

Satisfies the specification
Doesn’t satisfy the specification

Answer.

ii is correct.

Solution.

Suppose that the input list were [2, 8]. Our procedure will return 5, which isn’t on the list, nor is it even.