Gregory M. Kapfhammer

Associate Professor of Computer Science

http://www.cs.allegheny.edu/~gkapfham/

  
View  Edit  Uploads  History  Top  Changes  Search

A Specificier's Introduction to Formal Methods

  • Provide a definition of the term "specification language." Give an example use by the authors to explain the notion of a specification language. What other examples of specification languages can you provide?


A specification language is simply a mathematical notation, which is the syntactic domain. It has a universe of objects that is its semantic domain and there are precise rules that define which objects satisfy each specification. Z is an example used, that is based on set theory. There is a model oriented speicfication of a symbol table that uses Z notation. The table is modeled by a a partial mapping from keys to values.

I could not think of any specification languages off the top of my head so I searched the internet. I found a specification language called ALD/C++. It associates behavior specifications as post-conditions with C++ function declarations. It has a clean subset of the C++ expression language and its semantics are simple and informal. The important features of C++ such as member functions, virtual members, constructors, inheritance and exceptions are specified in ADL/C++. This specification language seems very useful.
Joe Zumpella

What is the purpose of this specification language? Is it simply there so that programmers can clearly state the intent of the methods in their programs? Or, is the specification language really used by a program that can check that the method's code will meet the stated design contract? Or, is there a runtime infrastructure that actually checks to see if the method's contract is enforced at runtime? Can you provide a link to this specification language? Greg

I would say that a specification language is any standard notation that uses a defined syntax along with a defined semantics to create a formal method's mathematical basis.

The authors point out that Backus-Naur form is a specification language with its own set of grammars making up its syntactic domain and a set of strings making up its semantic domain.

Any programming language can be considered a specification language.

Matt DeNapoli

Yes, you are right that any programming language can be considered a specification language. But, it is important to remember that the reverse is not true! That is, a specification does not have to be executable on a computer (in fact, it might specify something that is not computable!). Also, Wing asserts the following: "The question is whether they work with informal requirements and formal programs, or whether they use additional formalism to assist them during requirements specification?" How would you respond to this assertion? Greg

A specification language is a mathematical notation, a set of objects and a satsify rule that together make up the mathematical basis for a formal method. The notation is it's syntactic domain; the set of objects, it's semantic domain, and there is a satisfying relationship between the two.

To expand on Backus-Naur, mentioned by Matt, any string genereated by a grammar can be considered a specificand, and every set of these strings is considered a formal language. So Backus-Naur is considered a formal specification language for producing formal languages.

Other types of specification languages include those for algebras, distributed systems, programming languages, and many others.

Richard Geary

The set of strings that are generated by the grammar are one part of the three-tuple that makes up a specification language. We also need to have the Syntactic Domain and the Satisfies relation. One final interesting question: why did Wing state that Sat was a relation and not a function? What does it mean when we state that something is a function? Greg

  • What are the two main properties of specifications with which we should concern ourselves?



The two most important properties are having the language be defined so each well-formed specification is unambiguous. The other main property is having a language that has consistency. This property shows that there is some implementation that satisfies the specification. Joe Zumpella

The first main property of a specification is that it is unambigous, meaning it only has one meaning. The other main property is consistency, meaning that there is an implementation to realize the specification and that implementation will only produce non-contradictory (non-mutually exclusive) answers.

Matt DeNapoli

As mentioned by Joe and Matt, the two big properties are unambigious and consistent. To be unambiguos means that the language must never have two different semantic interpretations of any specificand.
Consistency means that there must be an implementation for every possible spcification, and also, that there are never two impementations that logically contradict each other.

Richard Geary



Implementation bias is when there is too little design freedom for the implementer and in other words, the specification is overspecified.

It can be related to the good requirements in chapter 8 by using the principles of concise, precise, and clear. These properties force the developer to specify in great detail. If they are over precise and clear they can leave the implementer with too little freedom.
Joe Zumpella

Implementation bias occurs when the specification forces the implementation. In other words, overspecification causes the implementer to be locked in to a set way of implementing the specification because the specification puts too many unneeded constraints on its specificands and thus on the implementer.

I think this is related to the complete property of good requirements. Completeness of a specification is a fine line. Not enough information, and the implementer chooses a bad, or incorrect, implementation that may not meet the specification. Too much, and the implementer is locked into the specifiers idea of implementation, preventing leeway for the implementer and introducing implementation bias.
Matt DeNapoli

Simply put, a specification that is too involved, too detailed, it may leave the implemetnor no choice but to choose a certain "way" of doing things, because any other choice would fail to meet the requirements.

This is directly related to the 'Nonprescriptive requirement" of Chapter 8. Nonprescriptive specifically says that a specification should state what should be done, not how it should be done. As soon as that line is corssed, implementation-bias occurs.

Richard Geary

  • Wing asserts that there are challenges that must be overcome by formal methods researchers and practicioners. What are these challenges? Which challenge do you think is the most important to overcome first?

Wing talks about many different bounds. He talks about the boundaries between the mathematical world and the real world. The problem here is that the specifier needs to specify exactly what the customer wants. Communication is key here and without good communication the customer might not get what they really want. Another boundary is the boundary between the real system and the environment. Often the environment can't be predicted and sometimes the formal methods leave out specification about the environment. This can cause problems if the user's input is incorrect. He also talked about pragmatic bounds that that researchers are trying to overcome. They are trying to better specify issues or reliability, safety, real time, and human factors. They are trying to combine different methods and building more usable and robust tools. Also reusing terms and their components by having specification libraries. They also would like to train more people to use formal methods.

Of all of these different problems I think they need to solve problems with communication and the environment. I think that they both go hand in hand. I think that if there is good communication between the customer and the developer then problems with user input can be solved. The customer needs to specify what kind of environment the project is going to placed in so the developer can create the best specifications for the project. I think this problem can cause the most damage and if it becomes fixed then most of the other problems will be solved. Joe Zumpella

"Jeanette Wing" -> "She" ! Greg

The first challenge Wing points out is the difference between the ideal and real worlds and the muddledness that is encountered between customer and the specifier. Another challenge comes in the environment which the specified system is subject to. The system is affected by its environment, thus it is necessary to take into consideration the environment itself.. Other challenges Wing points out include: specifying non-functional behavior of the system, combining different methods, robust usability tools for specification management, specification libraries for reuse, formal methods for all phases of software development, new techniques, more use.

The challenge of creating a clear link between the customer and the specifier is one that would have to be tackled first. Because formal methods are currently in use, it is only necessary that any system created meet customer requirements. For that to happen though, the customer has to relay there requirements in a clear and concise manner to the specifiers so that nothing is lost in the process.

Matt DeNapoli

As Joe and Matt have already stated, the main concerns that the author explains in detail are the overcoming the bounds between the mathematical and real world, the bounds between the real world and an abstract representation of the real world, and the bound between a real system and it's environment.

While all of these are pretty important, my gut instinct tells me that the first two are more important than the last. Getting user requirements to be accurately represented in a mathemaical way, and then "approximating" the real world in an abstract way are very very important for a specification language. It seems to me, that this is the very reason that specification languages exist. These concerns should be put above others.

Richard Geary

Link to this Page