What are your arguments about myths of formal methods?

• Formal methods can guarantee that software is perfect. 
• They work by proving that programs are correct. 
• Only highly critical systems benefit from their use. 
• They involve complex mathematics. 
• They increase the cost of development. 
• They are incomprehensible to clients. 
• Nobody uses them for real projects. 

Activities of Formal Methods

• Writing a formal specification
• Proving properties about the specification
• Constructing a program by mathematically manipulating the specification
• Verifying a program by mathematical argument

Key points

• Formal system specification complements informal specification techniques.
• Formal specifications are precise and unambiguous. They remove areas of doubt in a specification.
• Formal specifications force an analysis of the system requirements at an early stage. That helps us in correcting errors at this stage is cheaper than modifying a delivered system.
• Formal specification techniques are most applicable in the development of critical systems and standards.
• Algebraic techniques are suited to interface specification where the interface is defined as a set of object classes.
• Model-based techniques model the system using sets and functions. This simplifies some types of behavioural specification.

Limitations to Formal Methods

• Use formal methods as supplements to quality assurance methods not a replacement for them
• Useful for consistency checks, but formal methods cannot guarantee the completeness of a specifications
• Formal methods must be fully integrated with domain knowledge to achieve positive results

Acceptance of formal methods

• Formal methods have not become mainstream software development techniques as was once predicted
• Other software engineering techniques with better quality results. 
• Time-to-market versus high quality
• Hard to scale up to large systems
• Not well-suited for specifying and analysing user interfaces and user interaction

Question#4:   (15)
Defines a binary search tree where the data is of generic type Elem.
Build is an additional primitive constructor operation which is introduced to simplify the specification. It builds a tree given the value of a node and the left and right sub-tree.

Add(Binary_tree, Elem)	Adds a node to the binary tree using the usual ordering principles
Left(Binary_tree)	Returns the left sub-tree of the top of the tree
Data(Binary_tree)	Returns the value of the data element at the top of the tree
Right(Binary_tree)	Returns the right sub-tree of the top of the tree
IsEmpty(Binary_tree)	Returns true of the tree does not contain any elements
Contains(Binary_tree, Elem)	Returns true of the tree contains the given element

Solution:

Signatures

Create => Binary_tree
Add(Binary_tree, Elem) => Binary_tree
Left(Binary_tree) => Binary_tree
Data(Binary_tree) => Elem
Right(Binary_tree) => Binary_tree
IsEmpty(Binary_tree) => Boolean
Contains(Binary_tree, Elem) => Boolean
Build(Binary_tree, Elem, Binary_tree) => Biniary_tree

Axioms

We need to specify a Binary Search Tree,its signature is given below,Write axioms to complete Specification.Write down the Axioms for Binary Search Tree?

Add (Create, E)                    =  Build(Create, E, Create)

Add (B, E)                            =  if E < Data (B) then Add (Left(B), E)

                                                  else Add (Right (B), E)

Left (Create)                      = Create

Right (Create)                    = Create

Data (Create)                     = Undefined

Left (Build(L, D, R))         = L

Right (Build(L, D, R))       = R

Data (Build(L, D, R))        = D

IsEmpty(Create)                = true

IsEmpty (Build (L, D, R)) = false

Contains (Create, E)          = false

Contains (Build (L, D, R), E)           = if E = D then true

                                                             else if  E < D then Contains (L, E)

                                                                          else Contains (R, E)

Question#3: (15)
A video rental company keeps a data base of its customers & classifier then as good, bad or Ugly. Every customer is classified as exactly one of these. For each customer there is a record of which videos he or has out & a record of which of these are over rude. Each customer has unique ID call the customer set C,G, B & U respectively.

(a) Write a Z-schema for a Person & for database including invariants to specify this.

(b) Write pre & post condition for a routine that transfers a given customer & from G to B, assuming that the customer is originally in G.

(c) Write conditions for the above routine without assumption of pre-condition: true?

Question#2:           (15)
With respect to petri-nets which of transitions are enabled for firing?
For enabled transitions,Show results of firing?

(a) 2 1 0 0

->  0 0 1 1

(b) 3 1 0 0

->  1 0 1 1

(c) 1 1 0 

->  1 1 0






A & B are enabled for firing

Question#1:  (15)

We need to specify an abstract data type to represent music that can be sung by a single voice. In Keeping with standard musical terminology, we will call this ADT property, but in our simplified view of the world, a voice is basically just a sequence of notes & rests. The signature part along with informal specification of the algebraic specification for the ADT is given below:

1.       Emptyvoice: Creates an empty voice that is a voice without any notes in it.

2.       oneNote: Creates a voice made up of only one note

3.       Concatenate :Creates a voice by concatenating two voices  together

4.       Is_empty :Checks if a voice is empty

5.       firstNote :Returns the first note of voice.

Solution:

Emptyvoice:   => voice
oneNote:   Note => voice
Concatenate:  voice,voice  => voice
Is_empty :  voice => Boolean
firstNote : voice => Note
otherNotes: voice => Note

   Write Axioms to complete specification?

Specifying isEmpty is straightforward:
isEmpty (emptyVoice ()) = true
isEmpty (oneNote (n)) = false
isEmpty (concatenated (v1,v2)) = isEmpty (v1) & isEmpty (v2)

Specifying firstNote is just a bit more interesting:
firstNote (emptyVoice ()) = error

firstNote (oneNote (n)) = n
firstNote (concatenated (v1,v2)) =
              firstNote (v2) if isEmpty(v1)
               firstNote (v1)           otherwise

firstNote when applied to an empty voice. it should be an error.

otherNotes (oneNote (n)) = emptyVoice ()
otherNotes (concatenated (v1,v2)) =
                  otherNotes (v2) if isEmpty(v1)
                  concatenated (otherNotes (v1),v2)          otherwise

firstNote (otherNotes (concatenated (oneNote (n1), concatenated (oneNote (n2), oneNote (n3)))))
= firstNote (concatenated (otherNodes (oneNote (n1)), concatenated (oneNote (n2), oneNote (n3))))
= firstNote (concatenated (emptyVoice (), concatenated (oneNote (n2), oneNote (n3))))
= firstNote (concatenated (oneNote (n2), oneNote (n3)))
= firstNote (oneNote (n2))
= n2