Talk:Formal methods

From Wikipedia, the free encyclopedia
Jump to: navigation, search
WikiProject Computer science (Rated Start-class, Top-importance)
WikiProject icon This article is within the scope of WikiProject Computer science, a collaborative effort to improve the coverage of Computer science related articles on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.
Start-Class article Start  This article has been rated as Start-Class on the project's quality scale.
 Top  This article has been rated as Top-importance on the project's importance scale.
 

Model Checkers[edit]

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[edit]

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.

Formal methods[edit]

Verification[edit]

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[edit]

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

Please add machine checkable proofs[edit]

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[edit]

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[edit]

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)
Also, totally agree. I've found this on other IT articles as well, writing the article as if it has to present the two most extreme views of the subject (e.g. OOP solves all software problems! vs. OOP is rubbish!) the emphasis IMO shouldn't be on presenting the debate between the most vociferous advocates and detractors but in objectively describing the pros and cons. --MadScientistX11 (talk) 16:29, 14 February 2014 (UTC)

Criticisms Section Contains Facts, Not Criticisms[edit]

  • "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?[edit]

"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[edit]

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"[edit]

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[edit]

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)

Proposed merge with Formal methods and large scale systems[edit]

I don't really see why a separate article about FM in large systems is needed; also, Formal methods and large scale systems has some pretty generic examples of FMs in practical use. QVVERTYVS (hm?) 16:08, 14 February 2014 (UTC)

Makes sense to me. I support the merge. --MadScientistX11 (talk) 16:22, 14 February 2014 (UTC)
It looks like there is no Formal methods and large scale systems article anymore, it looks red to me, so I'll remove the merge notice since it makes no sense to merge without something that doesn't exist anymore, right? Sofia Koutsouveli (talk) 23:57, 17 March 2014 (UTC)
Indeed, and thanks for that, but I'm going to contact the admin who removed the other article. It had some content that deserved merging here. QVVERTYVS (hm?) 09:48, 18 March 2014 (UTC)

Proposed merge with Formal Methods and Data Intensive Systems[edit]

Recreation of Formal methods in large scale systems, discussed earlier. QVVERTYVS (hm?) 10:16, 19 March 2014 (UTC)

The article Formal methods in large scale systems seems to be deleted again which is IMO as it should be. I don't see the point in bringing back an article because you think some parts of it were worth merging into an existing article. If you think that then just rewrite the Formal methods article and add the new stuff. But I'm against bringing back that other article, it had a tag on it that indicated it was more a personal recollection and it clearly just overlaps this article. MadScientistX11 (talk) 12:45, 19 March 2014 (UTC)
The thing is that I'm not really familiar with the topic and the author of the other article seems to be so. Now, his material is all gone, including all of the examples of real-world applications of formal methods and a host of references to relevant work. QVVERTYVS (hm?) 14:12, 19 March 2014 (UTC)
Is there a way to look at that old article without recreating it? I am familiar with the topic, not an expert as some of the people who contributed are but I've done some formal methods work in the real world and read a fair bit of the literature. I could take a look at the old article and see if there is anything that stands out as really needing to be brought back. My guess is that there isn't much that was lost, the merge process is supposed to take care of that, before the article was deleted anything that other editors thought worth saving would have been put into this article. But I'm willing to take a look but I don't know how to see that deleted article. BTW, another thing that could be done is to create a user file with the old article and leave a comment in the Talk page with a link to that file. I would be more comfortable with that kind of a solution because a user page is not part of the encyclopedia. MadScientistX11 (talk) 14:28, 19 March 2014 (UTC)
I think you have to be an admin to see deleted pages. The other option is to request undeletion while promising to userfy the page to your own space. QVVERTYVS (hm?) 15:03, 19 March 2014 (UTC)
The merge proposal that was just set up doesn't work properly, it just links back to the same article as the article that is proposed for merger. Essentially, it's a proposal to merge the article with itself -- which is rather interesting from a formal methods perspective, a probably correct meaning preserving transformation ;-) but not something that I think should be kept. If someone can give me a link to the old article, I will create a new talk section and save that old article in a user page under my namespace (of course if someone else wants to do that so much the better) so that the content isn't lost and can be merged back in as appropriate but I continue to think it's not a good idea to recreate the deleted article. To do that we are essentially starting the merge discussion all over again. I'm not convinced it's even worth the trouble so I'm not going to spend time contacting an admin and doing that part myself. MadScientistX11 (talk) 17:44, 19 March 2014 (UTC)
That's because I already redirected the other article here after merging the main stuff. You need to look at the latest version as a full article. QVVERTYVS (hm?) 21:32, 19 March 2014 (UTC)
Btw. the other article wasn't deleted at all. QVVERTYVS (hm?) 21:32, 19 March 2014 (UTC)
Now that I've actually read the article I really don't understand why you are putting any effort into this. The page you linked to is poorly written and comes off as some bachelor's student in computer science who has gone through one formal methods class. It adds nothing and IMO parts of it are simply wrong. Talking about how even small problems in large scale systems somehow means that formal methods are appropriate is not accurate. I know people who are strong proponents of formal methods and even they would say as much. Formal methods aren't justified or very useful in making some transaction or Internet system a few percentage points more efficient. Where they are valuable is in things like mission critical software, weapons or security where one mistake can mean you lose lives or someone cracks your code. Or in the design of hardware where a mistake means you have to remake the chip. And the stuff that wasn't wrong was just boilerplate that is already in this article and written in a more professional way than that one was. MadScientistX11 (talk) 23:55, 19 March 2014 (UTC)
It's the references more than the text (which is largely a sales pitch for the author's own publications): the other article cites examples of where formal methods were used in industrial practice, something that was entirely missing from this article. I think I merged the most important bits now. QVVERTYVS (hm?) 13:23, 20 March 2014 (UTC)