Talk:Formal methods
From Wikipedia, the free encyclopedia
Proponents and critics are the same peoples.
So article is incorrect.
How can a discussion of software development processes not include the Unified Process? A complete discussion of XP but not one mention of UP. Biased in my opinion.
- RUP is not a formal method. RUP has no theorem prover. RUP has no Z-like notation. Just writing prose requirements is not "formal". —optikos 16:27, 5 November 2006 (UTC)
Contents |
[edit] Old Example
I'm not sure this example is really appropriate; it's one specific method out of many. At a minimum, the tone is too informal. I'm going to move it here for now and perhaps work on incorporating it later. Jim Huggins 21:32, 26 Apr 2005 (UTC)
Thowa 10:42, 17 Apr 2005 (UTC): None of the formal methods can be shortly explained within a Wiki-discussion. But let's do a short example, a more interested reader might find as a useful starting point to understand how powerful formal methods in practise are.
Let's create a finite state machine (FSM) having two states "Eat" and "Sleep". This FSM shall communicate with two external objects: a digital input (di) and a timer (ti). The digital input can generate two signals: “true” and “false”. The timer generates one signal “over”. The timer accepts also a command “start” (which does a reset and starts the timer). We create an input and output dictionary which can be used by the FSM:
- Input dictionary
- {di_true, di_false, ti_over}
- Output dictionary
- {ti_start}
What does our example FSM do? It starts in state “Eat” and goes to state “Sleep” in case the di was set to “true”. Entering the state “Sleep” the FSM starts the timer. To go back to state “Eat” the timer must be “over” (ti_over) and the di must be changed to “false” (di_false). Please print the FSM transition diagram on a piece of paper to avoid any misunderstanding. To create the executable specification we need to create state transition tables for each state of our FSM:
| State Name | Condition(s) | Actions(s) |
|---|---|---|
| Eat (current state) | Entry action | n/a |
| Sleep (next state) | di_true | n/a |
and
| State Name | Condition(s) | Actions(s) |
|---|---|---|
| Sleep (current state) | Entry action | ti_start |
| Eat (next state) | di_false AND ti_over | n/a |
An automatic process can generate a set of equations which fully express the above specification. This set could look like this (note that this is already a kind of machine code, so it looks criptical, but I enter it here to show the “magic” behind the executable specification):
S1 N2 V4 S2 E1 N1 V3&2
where S represents the current state, N the next state, E entry action and V condition (& means AND). For instance the first line means “in state 1 (Eat) go to state 2 (Sleep) if the boolean condition 4 (di_true) is true”.
Some words about the used boolean algebra here. In the presented concept it is the positive logic algebra and not the boolean algebra (i.e. NOT is forbidden). The reason is simple: in the software world we have very seldom signals which can be negated. Lets take for instance a sensor which delivers temperature: temp_low, temp_good and temp_high. What would be NOT temp_high? So in the above concept we only look if a signal exists or not. Some signals cannot exists in parallel, e.g. We cannot have at the same time di_true and di_false.
The above equation plus the description of the I/O dictionaries can be now read by a standard executor (which might be a part of the OS) and executed.
[edit] Formal methods
[edit] Verification
It is true that an automated theorem-prover requires human assistance simply because the logic is (normally) too expressive, but what is the rationale for claiming that model-checking approaches "quickly get bogged down in checking millions of uninteresting states if not given a sufficiently abstract model"? What is a "sufficiently abstract model"? What does it mean to get "bogged down"? Finally, why does it matter? // Mats Kindahl 06:28, 19 June 2006 (UTC)
- This was presumably written by someone trying to provide a "balanced point of view". But I agree that the statement isn't particularly clear or useful. It'd probably be better to substitute a (referenced) sentence that describes the weaknesses of model-checking. --Allan McInnes (talk) 15:29, 19 June 2006 (UTC)
[edit] References
- Moved from article --Allan McInnes (talk) 18:44, 23 December 2006 (UTC)
I am missing a number of references:
1. David Gries, the science of programming 2. C. Hoare, lots of articles about proving programs 3. E. Dijkstra, another writer who has written a lot about proofing programs, especially about semaphores and such. —The preceding unsigned comment was added by 86.87.79.130 (talk • contribs).
[edit] Please add machine checkable proofs
What seems to be missing in this article is the middle ground between hand-written mathematical proofs and automatic theorem proving. The interactive theorem provers like Isabelle, Coq, etc. allow writing proofs that are machine checkable. -- Hritcu 11:17, 22 January 2007 (UTC)
- Please feel free to add any material you think the article is missing. --Allan McInnes (talk) 04:11, 23 January 2007 (UTC)
[edit] Type Systems
Formal methods are not only about correctness. Type systems are also considered (lightweight) formal methods, and their goal is to prevent runtime errors by static analysis. There are many other static analysis methods. -- Hritcu 11:54, 22 January 2007 (UTC)
- I'm not sure that I see the distinction you are trying to make here. A well-typed program is "correct" in the sense that it does not have any type inconsistencies. As a consequence of that correctness, it will not produce runtime type errors. If your concern is that the article doesn't mention type systems and other static analysis methods, then I agree that it would be good to have some discussion of such things. --Allan McInnes (talk) 04:26, 23 January 2007 (UTC)
[edit] Change of tone - there is no fight
Personally I don't like the tone of the article, which presents formal methods like some very controversial topic people are arguing about. Sure there are proponents, and critics, but the article focuses almost entirely on this debate. Like the article mentions, by now people have very much understood that formal methods are no silver bullet. They have advantages and disadvantages and they are all quite well understood. Why not have the focus on advantages/disadvantages rather than on pointless flamewars. -- Hritcu 11:17, 22 January 2007 (UTC)
- I wholeheartedly agree. --Allan McInnes (talk) 04:28, 23 January 2007 (UTC)
[edit] Criticisms Section Contains Facts, Not Criticisms
- "internal criticisms" ? What does this mean?
- proving correctness requires a long time (and time means money) - duh, it is a fact not a criticism, like all the other statements in this section. Sure, it would be nice to have references for these claims, but they seem pretty much common sense, and they are not critical, to justify having them in a criticisms section. On the other hand the article is full of "critics say" statements which would very well suit this section, since they make the article look like a slashdot discussion not an encyclopaedia entry. -- Hritcu 11:31, 22 January 2007 (UTC)
