Tuesday, January 28, 2014

The advantages of inspections over testing

Many defects found in testing are directly traceable to requirements and design flaws that
could have been detected earlier


1.Defects that are found later in the project will not only cost
more to fix, but also work that are from incorrect design and/or requirements are wasted
2.The strengths of
inspections are that a similar process can be applied to a wide range of documents
3.It can it be much easier to find
faults in code standard and traceability with inspection than it is with testing This is because
inspection will find the fault in the code and testing will only find the failure
4.The first is that inspection can found many defects in a single inspection session

Inspection vs Testing

Monday, January 27, 2014

Formal Method Z notation of Print spooler

Click Here to download file


The state
used, free: P BLOCKS
BlockQueue: seq P BLOCKS


Data Invariant
used > free = \
used < free  =  AllBlocks
 i: dom BlockQueue  BlockQueue i # used
 i, j : dom BlockQueue  i ≠ j => BlockQueue i > BlockQueue j = \


Precondition
         #BlockQueue > 0


Postcondition
used' = used \ head BlockQueue   
free’ = free < head BlockQueue 
BlockQueue' = tail BlockQueue

Formal Method (object constraint language) of Print spooler



Click here to download file


No block will be marked as both unused and used.
  context BlockHandler inv:
    (self.used->intersection(self.free)) ->isEmpty()
All the sets of blocks held in the queue will be subsets of the collection of currently used blocks.
  context BlockHandler inv:
    blockQueue->forAll(aBlockSet | used->includesAll(aBlockSet ))
No elements of the queue will contain the same block numbers.
  context BlockHandler inv:
    blockQueue->forAll(blockSet1, blockSet2 |
      blockSet1 <> blockSet2 implies
      blockSet1.elements.number->excludesAll(blockSet2.elements.number))
The expression before implies is needed to ensure we ignore pairs where both elements are the same Block.
The collection of used blocks and blocks that are unused will be the total collection of blocks that make up files.
  context BlockHandler inv:
    allBlocks = used->union(free)
The collection of unused blocks will have no duplicate block numbers.
  context BlockHandler inv:
    free->isUnique(aBlock | aBlock.number)
The collection of used blocks will have no duplicate block numbers.
  context BlockHandler inv:
    used->isUnique(aBlock | aBlock.number)

Formal Method of print spooler

A Print Spooler. In multitasking operating systems, a number of tasks make requests to print files. Often, there are not enough printing devices to satisfy all current print requests simultaneously. Any print request that cannot be immediately satisfied is placed in a queue awaiting printing. The part of an operating system that deals with the administration of such queues is known as a print spooler.

In this example we assume that the operating system can employ no more than MaxDevs output devices and that each device has a queue associated with it. We will also assume that each device is associated with a limit of lines in a file which it will print. For example, an output device that has a limit of 1000 lines of printing will be associated with a queue that contains only files having no more than 1000 lines of text. Print spoolers sometimes impose this constraint in order to forbid large print jobs that may occupy slow printing devices for exceptionally long periods. A schematic representation of a print spooler is shown in figure.

Referring to the figure, spooler state consists of four components: the queues of files waiting to be printed, each queue being associated with a particular output device; the collection of output devices controlled by the spooler; the relationship between the output devices and the maximum file size that each can print; and the relationship between the files awaiting printing and their size in lines. For example, figure shows that the output device LP1 which has a print limit of 750 lines has two files ftax and persons awaiting printing, and that the size of the files are 650 lines and 700 lines, respectively.

The state of the spooler is represented by the four components: queues, output
devices, limits, and sizes. The data invariant has five components:
Each output device is associated with an upper limit on print lines.
Each output device is associated with a possibly nonempty queue of files awaiting printing.
Each file is associated with a size.
Each queue associated with an output device contains files that have a size less than the upper limit of the output device.
There will be no more than MaxDevs output devices administered by the spooler.

A number of operations can be associated with the spooler. For example,
An operation that adds a new output device to the spooler together with its associated print limit.
An operation that removes a file from the queue associated with a particular output device.
An operation that adds a file to the queue associated with a particular output device.
An operation that alters the upper limit of print lines for a particular output device.
An operation that moves a file from a queue associated with an output device to another queue associated with a second output device.

Each of these operations corresponds to a function of the spooler. For example, the first operation would correspond to the spooler being notified of a new device being attached to the computer containing the operating system that administers the spooler.

As before, each operation is associated with a precondition and a postcondition. For example, the precondition for the first operation is that the output device name does not already exist and that there are currently less than MaxDevs output devices known to the spooler. The postcondition is that the name of the new device is added to the collection of existing device names, a new entry is formed for the device with no files being associated with its queue, and the device is associated with its print limit.

The precondition for the second operation (removing a file from a queue associated with a particular output device) is that the device is known to the spooler and that at least one entry in the queue is associated with the device. The postcondition is that the head of the queue associated with the output device is removed and its entry in the part of the spooler that keeps tracks of file sizes is deleted.

The precondition for the fifth operation described (moving a file from a queue associated with an output device to another queue associated with a second output device) is
The first output device is known to the spooler.
The second output device is known to the spooler.
The queue associated with the first device contains the file to be moved.
The size of the file is less than or equal to the print limit associated with the second output device.

The postcondition is that the file is removed from one queue and added to another queue.

In each of the examples noted in this section, we introduce the key concepts of formal specification. But we do so without emphasizing the mathematics that are required to make the specification formal. In the next section, we consider these mathematics.