Brontekst bekijken van Taxonomy/1. Quality/90. Quality criteria

<noinclude>{{Taxonomy/Contents}}</noinclude>
{{Taxonomy/Intro|To answer this question, we broke it down to sub-questions and sub-sub-questions. Our quest lead us for example along a notion {{*|specification}}. We investigated how a specification is related to the [[property|properties]] it specifies, to an {{*|artefact}} that implements it, and to a {{*|blueprint}} of that artefact. We understood how specifications are targets of the activities to [[Taxonomy/supplement/Specify|Specify]] and to [[Taxonomy/supplement/Verify|Verify]] and starting points for the activities to [[Taxonomy/supplement/Validate|Validate]] and to [[Taxonomy/supplement/Design|Design]]. Of course, a ''good'' specification must be one that facilitates these activities. This gives rise to a taxonomy of straightforward quality criteria for specifications.  Mutatis mutandis, we can derive quality criteria for all [[Taxonomy/supplement/Object|Object]]s and [[activity|activities]] by studying how they are related to other objects and activities. In this way, our considerations about the [[Taxonomy/1._Quality/1._Rationality|Rationality Square]], [[Taxonomy/1._Quality/2._Models|Models]], [[Taxonomy/1._Quality/3._Formal_Methods|Formal Methods]], [[Taxonomy/1._Quality/4._Correctness_Theorems|Correctness Theorem]]s, [[Taxonomy/1._Quality/7._Development|Development]], and [[Taxonomy/1._Quality/8._Verification_and_validation|Verification and validation]] lead to the quality criteria presented here.}}

How can we discern quality around [[Taxonomy/1._Quality/7._Development|Development]], [[Taxonomy/1._Quality/8._Verification_and_validation|Verification and validation]] of artefacts?

When quality can be graded one-dimensionally, higher numbers in the lists below denote higher quality. 

== The playing field ==

=== Quality criteria for problems ===
A problem of high quality can still be very difficult to solve.
# There is no [[Taxonomy/2._Methodology/2._Problem_Statement|Problem Statement]], but we are already working on a solution.
# There is no [[Taxonomy/2._Methodology/2._Problem_Statement|Problem Statement]], but the first step will be to define one.
# From the [[Taxonomy/2._Methodology/2._Problem_Statement|Problem Statement]] follows that domain experts are necessary, but these are not available or unwilling to share their knowledge.
# Domain experts are available and willing, but neither can they understand the relevant specification and blueprint languages nor do they want to.
# Domain experts are available and willing, they are also prepared to communicate with the developer about the necessary specifications and blueprints, but the problem is a [[Taxonomy/supplement/Mean_problem|Mean problem]].
# Domain experts are available and willing, they are also prepared to communicate with the developer about the necessary specifications and blueprints, and the problem is a [[Taxonomy/supplement/Tame_problem|Tame problem]].

=== Quality criteria for the [[Taxonomy/supplement/problem domain|problem domain]] ===
# There is only a vague idea about the problem domain, there are no experts, and nobody knows whether there are useful [[theory|theories]].
# There are [[Taxonomy/supplement/Domain_expert|Domain expert]]s, but there is little or no [[Taxonomy/supplement/Theory|theory]].
# There are [[Taxonomy/supplement/Domain_expert|Domain expert]]s and there is enough [[Taxonomy/supplement/Theory|theory]].
# There are [[Taxonomy/supplement/Domain_expert|Domain expert]]s and there is a {{*|specification language}} based on the necessary [[Taxonomy/supplement/Theory|theory]].
# There are [[Taxonomy/supplement/Domain_expert|Domain expert]]s and there there are [[Taxonomy/supplement/Tool|tool]]s for the corresponding {{*|specification language}}.
# There are [[Taxonomy/supplement/Domain_expert|Domain expert]]s and there there are [[Taxonomy/supplement/Tool|tool]]s that even connect the {{*|specification language}} to a [[Taxonomy/supplement/solution domain|solution domain]].

=== Quality criteria for the solution domain ===
With low-quality solution domains it can seem easy to solve a problem, but the quality of the solution will be low.
# The [[Taxonomy/supplement/solution domain|solution domain]] is fixed, it provides [[part]]s from which the solution has to be built, but these are ill-specified and/or the necessary [[Taxonomy/supplement/Theory|theory]] is missing. There are "domain experts". (Shoot them!)
# The [[Taxonomy/supplement/solution domain|solution domain]] is fixed, it provides well specified [[part]]s and the necessary [[Taxonomy/supplement/Theory|theory]].
# The [[Taxonomy/supplement/solution domain|solution domain]] is fixed and there is a [[Taxonomy/supplement/blueprint language|blueprint language]] based on the necessary [[Taxonomy/supplement/Theory|theory]]. 
# The [[Taxonomy/supplement/solution domain|solution domain]] is fixed and there is a [[Taxonomy/supplement/blueprint language|blueprint language]] based on the necessary [[Taxonomy/supplement/Theory|theory]], from which correct realisations can be derived automatically.
# The [[Taxonomy/supplement/solution domain|solution domain]] is fixed and there is a [[Taxonomy/supplement/blueprint language|blueprint language]] based on the necessary [[Taxonomy/supplement/Theory|theory]], from which correct realisations can be derived automatically. Moreover, there are verification tools.
# The [[Taxonomy/supplement/solution domain|solution domain]] is not fixed, but the solution has to be bound together with existing artefacts, the interface being well defined.
# The [[Taxonomy/supplement/solution domain|solution domain]] is completely open.

It may seem surprising that a completely open solution domain is better than an ill-defined one, which at least provides ready-made parts from the shelf. But if the solution domain is open, the designer can, of course, choose the best possible, with the least inhibitation of creativity.

Most programming languages favoured by IT-professionals are, alas, quality 1 solution domains.

== The means ==

=== Quality criteria for all languages involved ===
During half a century of research [[Taxonomy/supplement/Computer_Science|Computer Science]] has understood very well how to design and to define [[languages]]. Useful theory about the definition and transformation of languages and about fundamental language concepts has been developed, and there are good language processing [[tools]]. Also, there is a good common understanding of concepts and paradigms that should be supported in ''any'' language. A good language should...
* be syntactically well-defined by means of a grammar,
* have formally defined semantics, preferably fixed by an international standard.
* consist of a small kernel together with the possibility to define what is necessary ''in'' the language,
* provide a simple, logical and orthogonal notation,
* be orthogonal and consistent w.r.t. all concepts in the kernel,
* make parsing easy,
* make use of a powerful but friendly typing system,
* provide a mechanism for modularity.

Although all this is well-understood, many widespread languages are far from this ideal. SQL is an example where nearly everything that can be wrong is wrong. PVS, on the other hand, meets most of these criteria but has such bizarre syntax that most of its charme is lost.

=== Quality criteria for specification languages ===
Quality of specification languages is a multi-dimensional issue, where the dimensions are conflicting. An ideal specification language should be, for example, [[declarative]] and [[executable]] at the same time–which is theoretically impossible. It should both be extensible and understandable at first glance. It should be so modern that it is based on theory which just has been detected at universities, but should at the same time have a fool-proof graphical interface, should "run" under Windows and be integrated with all existing tools. The ideal specification language cannot exist!

Nevertheless, here is a whish list. A good specification language for a certain [[Taxonomy/supplement/problem domain|problem domain]] should not only meet above criteria but moreover...
* have a semantics that allows to express the relevant {{*|property|properties}} in that [[Taxonomy/supplement/problem domain|problem domain]],
* provide the concepts and the notations familiar to [[Taxonomy/supplement/Domain_expert|Domain expert]]s or provide a mechanism that allows to define such concepts and notations,
* allow some form of simulation or rapid prototyping to support [[Taxonomy/supplement/Validation|validation]] of specifications,
* be based on a theory that provides rules to compare specifications,
* be supported by development and proof tools.

=== Quality criteria for blueprint languages ===

== The goal ==

{{Taxonomy/tired}}
=== Quality criteria for focus ===

horizontal, vertical

{{!|Hanno Wupper||Angelika's mail:

; problem: it is difficult to fix the environment completely. there are a few basic choices where we have to find the right balance:
# We assume an environment behaving "normal", e.g. no earthquakes, electricity available, no students sitting on relevant parts of the plant, gravity working as usual, or whatever.
# There is something we called "desired behaviour", that is what the overall system (physical+control) should do.
# There is something called the "uncontrolled behaviour". All possibilities that a plant can do.
; discussion:
*we should agree on basics as in 1) otherwise we end up in Michael Jackson's party game.
*for the batch plant we concentrated only on 2), the desired behaviour. also from our MOCA proposal  i remember the statement that the uncontrolled behaviour is simply too huge and we do not want to consider everything. for example, in the lego plant, the belt could also run backwards, in the batch plant the valves could also be open for every possible amount of time. and these things are somehow  not so interesting, so, why spoil time on this?
*if we only restrict to the desired behaviour our correctness theorem is possibly not correct. what does this say? In the lego-example we have: 1. a description of the plant according to the desired behaviour, 2. a description of a "correct" control, that composed with the desired plant behaviour satisfies the requirements, and 3. a description of an "uncorrect" control, that composed with the desired plant behaviour also satisfies the requirements, and this is what we certainly do not want to have.

altogether, there are 2 contradicting things we want to have: a description of the plant that is as short (and efficient) as possible, on the other hand we need sufficiently enough "undesired" behaviour of the plant, such that the composition with the control and its verification is indeed meaningful.
}}

{{!|Hanno Wupper|| 

; Where is the border between the {{*|artefact}} under discussion and its environment? : When we consider power supply as relevant, we can either assume that the environment provides it or consider an artefact that contains a battery or power station as a component.

; Which assumptions do we make about the environment? :

; gravity : This question can safely be left open until we make choices about our artefact's design. When we try to prove something we will be reminded which laws of nature are to be included in the model.

; earthquakes : In San Francisco and Tokio there are important and will often be mentioned in the highest level specification. In other places we may tacitly assume their trheat irrelevant.

;Which design?  : A bridge, tunnel, ferry, cable car or catapult? Do we have to make a choice immediately or can we better design them all in parallel until we are sure which designs will survive and which not?

;{{*|decomposition}} :

* interface points vs. parts
* recipe, batch, process 

}}

=== Quality criteria vor views ===
* Covers all aspects considered relevant.
* Abstracts from aspects not considered relevant.
{{!|Hanno Wupper|| Example: 
* If we are interested in the correctness of routing in a computer network we may decide to assume tacitly that all system components are supplied with electricity. Every decent computer room in a routing station nowadays has safe power-supply. We can take this for granted or leave it to the correctness theorem for another view. 
* If we want a correctness theorem for the roadies of a rock band we should better inlude power supply. Roadies have to connect all components by cables in exactly the right way. It does not make a difference whether an audio cable or a power cable is missing: the installation will fail.
}}

=== Quality criteria for correctness arguments ===
# There is no correctness argument.
# There is no correctness argument, but the artefact is the result of some slight changes to an artefact that had been considered correct.
# The artefact has been tested or its blueprint has been simulated. This challenge has not revealed faults.
# There is an informally stated correctness theorem, and there is a developer prepared to defend it.
# There is a formal correctness theorem without proof, and there is a developer prepared to defend it.
# A correctness theorem has been succesfully model checked.
# A correctness theorem has been proved by means of a proof tool, but the proof is too complex to be understood by human beings.
# There is a correctness theorem together with nice, comprehensible, convincing proof.
# There is a generic correctness theorem together with nice, comprehensible, convincing proof.


=== Quality criteria for specifications ===
Customer and designer must agree on some kind of specification of the system to be designed. In the weakest case that specification consists of no more than vague ideas in the customer’s and the designer’s heads, with the possibility of all kinds of misunderstandings. Ideally, it is in the interest of both parties to have a written specification, which can be used as a legal contract. The customer then does not need to fear to have to pay for a product he never wanted, while the designer does not have to fear that the customer will not pay if he should change his mind while the system is being developed. 

* '''Clarity.''' Vaguely in the head of a customer / in the head of a domain expert / written down in natural language / in e defined formal language
** As long as a specification is not formalised: Not so vague that different readers might understand it differently. Will have to be clarified if it contains vague terms.
** Suitable as a contract between [[Taxonomy/supplement/developer|developer]] and [[Taxonomy/supplement/customer|customer]].
** Readable in the culture of the customer or at least of his [[Taxonomy/supplement/Domain_expert|Domain expert]].
* '''Generality.''' Sufficiently general not to exclude possible solutions. Will have to be weakened if customer was too specific.
* '''Suitability for formal verification.''' When a blueprint language has been fixed: is there a set of proof rules? a proof tool?
* '''Realism.''' When a design has been chosen: provable from the design. Will have to bee weakened until an affordable design is found.
{{!|Hanno Wupper||From B&B:}}
* '''Criteria voor specificaties'''
** S0 Wat je opschrijft, mag niet ambigu zijn.
*** Dit betreft allereerst eenduidige syntax. Als een bewering twee verschillende syntaxbomen kan hebben moeten deze tenminste dezelfde semantiek hebben.
*** Dezelfde termen in een specificatie moeten absoluut dezelfde begrippen betekenen, ook al zijn die begrippen misschien nog niet gedefinieerd.
** S1 Een (blackbox-)specificatie gaat over het Wat, niet over het Hoe. De belangrijkste reden hiervoor is dat op deze manier geen alternatieven bij voorbaat worden uitgesloten. (Het Hoe betreft de onderdelen, die je in de blackbox view dus even niet ziet). Het is mogelijk naar een bekend hoe te refereren om een bepaalde kwaliteit te specificeren ("hoorbare muziek alsof een strijkkwartet in de kamer speelt"), maar dan moet duidelijk zijn dat andere realisaties (bijvoorbeeld met luidsprekers) niet uitgesloten zijn (in dit voorbeeld door het woordje "alsof" aangegeven).
** S2 Een specificatie specificeert een afgebakend systeem en juist niet diens omgeving. Hooguit maakt de specificatie expliciet ''aannames'' over de omgeving. Maar de specificatie moet zich lenen als opdracht voor een ontwerper die de omgeving niet kent.
*** Fout: beweringen over het te specificeren object en zijn omgeving onlosmakelijk te versmelten ("De voetganger drukt op de knop, waarop het stoplicht op rood springt; dan steekt de voetganger over."
*** Fout: kennis over de omgeving veronderstellen.
** S3 Begrippen of items in de specificatie blijven vaak bewust (een tijdje) ondergespecificeerd. D.w.z. je laat sommige begrippen nog een beetje "open" of "vaag" (een betere term is "kwalitatief", bijv. stroom) totdat je eraan toe bent ze optimaal precies te maken ("kwantitatief", bijv. 230V, 50 Hz, 10 mA). (Onderspecificatie geldt vaak tijdens het specificatieproces, maar meestal niet meer aan het eind!).
** S4 Volledige, afgeronde specificaties dienen zo precies te zijn als nodig voor de context van die specificatie. <br>Bijv. een contract moet zo precies zijn dat klant(en) en leverancier(s) heldere en niet mis te verstane afspraken kunnen maken.
** S5 Sommige items kun je bewust - expliciet - weglaten<br>informatie over het systeem die wel bekend is maar die in deze context niet relevant wordt gevonden. : Dit heet ook wel abstractie. Bijv: de stroom benodigd om een apparaat te laten werken kan wel of niet worden meegespecificeerd; dat is een keuze) Niet te verwarren met S3!
** S6 Gedrag dient gespecificeerd te worden in termen van expliciet aangegeven observaties (= metingen). Bij elk "interfacepunt" hoort zo'n meting te worden opgegeven. Dingen die men niet kan meten (bijv. "leven") hebben in een specificatie niets te zoeken.
** S7 Als je iets als een interface (of meetpunt) specificeert, neem je aan dat de details van het "hoe" van die interface niet relevant zijn. Bijvoorbeeld: een USB-contact kan als een interface worden gezien, maar het kan ook per pootje worden uitgemodelleerd.
* '''Criteria vor het ontwerp''', d.w.z. voor de onderdelen van een artefact en hun samenhang<br>Als we de blackbox open maken, zien we een aantal onderdelen. Bij elk onderdeel hoort een specificatie.
** O0 Onderdelen van het systeem moeten bewijsbaar bij elkaar passen en zo een geheel vormen (geheel = het systeem).<br>onderdeel 1 /\ onderdeel 2 /\ onderdeel 3 /\ ... => systeem
** O1 Vat samen waar het helpt<br>voeg dan een aantal onderdelen bij elkaar onder 1 onderdeel. : Een maximum van 7 sub-onderdelen naast elkaar per onderdeel/systeem is aan te bevelen.


=== Quality criteria for blueprints ===


* Suitable as a contract between [[Taxonomy/supplement/developer|developer]] and [[Taxonomy/supplement/supplier|supplier]].
* Realisable.
* Contains enough information for the proof of the [[Taxonomy/1._Quality/4._Correctness_Theorems|Correctness Theorem]].
* Does not contain unnecessary details.
* Readable in the culture of the [[Taxonomy/supplement/supplier|supplier]] or at least of his [[Taxonomy/supplement/Domain_expert|Domain expert]].


== The game ==

=== Quality criteria for methods ===

* Should only lead to a [[Taxonomy/1._Quality/4._Correctness_Theorems|Correctness Theorem]] meeting above quality criteria.
* Should not exclude useful design.
* Should (''quickly'') efficiently lead to a [[Taxonomy/1._Quality/4._Correctness_Theorems|Correctness Theorem]]
* Should be efficiently adaptable for changes, e.g. for product families and new developments.
* Should be clear enough to convince "others" that the model is "correct".