Talk:Formal methods

Model Checkers

One of the most important model checkers is Java Pathfinder. It should be added. — Preceding unsigned comment added by 190.84.60.204 (talk) 04:43, 7 June 2012 (UTC)

---

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)

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.

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)

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).

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)

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)

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)

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)

Few thoughts about your post:
1) I think it is nice to have the common sense ("fact") written for people who don't know the subject.
2) I disagree with you that it is a common sense. In fact, many Formal Methods' proponents preach for it being widely applied in any field, not only high risk systems. So I think Criticism is the right place for it.
3) I don't really follow your reasoning... You think it is a obvious "fact", but at the same time you say it require references.
4) In some cases, placing "critics say" is a nice way to show what opponents say about it, while showing NPOV. And I don't understand why you think an Encyclopedia can't show when something has disagreements (like widely using formal methods against not using it).SSPecter ^Talk|E-Mail ◆ _{17:50, 5 November 2007 (UTC)}.

This is criticism: "Of course, it is widely believed that there is no silver bullet for software development," And it is quite debatable. I mean, the software crisis is exactly that: lack of formality! —Preceding unsigned comment added by 128.62.163.208 (talk) 20:27, 25 July 2008 (UTC)

Who watches the watchmen?

"Verifying the verifier" is an instance of a deeper philosophical problem named "Who watches the watchmen?". So I added an interdisciplinary link to Quis custodiet ipsos custodes? in the text of the article. --Antonielly (talk) 18:15, 14 November 2008 (UTC)

Test-Driven Development

Should Test-driven_development be considered a newer formal method?

Crowne (talk) 22:03, 9 March 2009 (UTC)

Tests are a formal specification of behaviour -one's machines can read- but they tend to be unsuited for formal proofs of correctness, at least when procedural languages are used to write the tests. SteveLoughran (talk) 13:21, 10 March 2009 (UTC)

"the sub-discipline of programming language semantics"

This encroachment is contradicted by the ACM classification system where "formal methods" is only a level-4 leaf. It certainly does not include programming language semantics in the ACM classification. This article, as well as the associated Wikipedia categories have been written/populated by someone with an obvious vested interest in enlarging the meaning of "formal methods". It reminds me of those mathematician that try to include computational complexity theory in computability theory despite the fact that the common view in computer science (c.f. theory of computation, which mostly follows the ACM classification) is that the two are distinct. On this wiki a number of prominent computer scientists have been categorized as "formal methods people", from Alan Turing to Don Knuth, none of which identified themselves as such, nor did they work in this fields as usually defined; they would certainly be theoretical computer science people as that notion is used nowadays, but that's far wider category. Pcap ping 15:09, 23 August 2009 (UTC)

I think I've addressed the issue. I've used a book written by a "formal methods person" as source. Pcap ping 18:51, 23 August 2009 (UTC)

Level taxonomy

This article currently says that formal methods can be used at different levels, namely Levels 0 to 2. Does this leveling imply increasing quality of formal methods with respect to correctness? And if so, what is the difference in quality between Level 1 (formal development and formal verification) and Level 2 (theorem prover)? --Abdull (talk) 09:17, 11 September 2010 (UTC)