Top page of Prof. Partha's CDROM titled -- "The burden of proof"

The links and images will work only from the CDROM.

An informal look at formal methods -- A short course on formal methods.

Independent Verification and Validation (IV&V).

 

Warning -- Achtung -- Attention :
This is "work in progress" In fact, we have just started this compilation (after a lot of background work). This CD is just a "Proof of concept" CD. It is given to you just for preview purpose. Do not make copies or distribute just now.

My e-mail address has changed to :
drpartha@gmail.com
Please make note of this change, and use only my new address shown above.

(WARNING -- Some pages in this CDROM may still point to my old address. Please watch out !)

Version-date: 20060307

 

The burden of proof

Dr. S. Parthasarathy

drpartha@gmail.com

About the title
About this CD
Meet the author

This is just a proof-of-concept CD
for preview, comments and suggestions only.

Study material for The burden of Proof

 

This material is for personal, academic usage only.

  • This CDROM is a collection of tutorial material about proof of program correctness. Although this document does not claim to be an exhaustive collection of all the material and resources available on the web, it is very rich in content. Read it at leisure, and keep it handy for future reference.
  • Some of the hyperlinks in this CDROM will need an on-line connection to the Internet.
  • This is a "platform independent" CDROM. You can read this CDROM using any web browser (HTML 4.0 and CSS-2 compatible), and under any operating system. You will also need a suitable software plug in for reading PDF files.
  • This CDROM does not install any software or modify any of your files or directories by itself. It does not contain any active material i.e. any program or script which get automatically executed on your computer.
  • It would be a good idea to download the latest version of the files, especially those which contain programs and important tutorials.
  • The web keeps changing all the time. Do not be disappointed if some of these links do not work any more, when you look for them in the web.

    This CDROM has hyperlinks to a very large number of external sites. We have no control over the owners of these web sites. When we included these links, we visited every one of these sites. We also keep visiting these sites randomly. This CDROM is continuously updated on the basis of our experiences. Yet, some flaws may persist.If you find dead links, or inappropriate contents, please exhibit some social responsibility please inform the author immediately, so that the next version of this CDROM does not carry forward these flaws.

  • Please send your comments, suggestions and opinions about this page, to S. Parthasarathy
  • The date and important details about this CDROM are given in the Administrivia section.

 


 

The burden of proof

An important social message from Algologic
Meet the author
This report will try to clear the smoke which surrounds the most misunderstood and enigmatic phrase in computer science. Read on. There is lots of interesting discoveries waiting for you.

Preamble
(the main material is after the horizontal ruler line below)

About the title
About this CD
Main material on proof
Why is Linux good for me ?
Send us your suggestions and comments
Administrivia
An important social message from Algologic
Literature references
 

MAIN -- Study material on proof

What is proof of program correctness ?
Foundations and background
Others sections to be added progressively
Logic and fallacies
The lighter side of proof
Literature references

The burden of proof

About the title

This report will try to clear the smoke which surrounds the most misunderstood and enigmatic phrase in computer science:
 

proof of program correctness


Except the two-letter word of, it is not easy to define or describe the meaning of the other words in the above phrase. By extension, it is just as difficult to explain the meaning of the entire phrase itself. A whole flood of literature is available on subjects related to the above phrase. Unfortunately, the literature is just as precise as the seven wise blind men who went to see an elephant. We can at best start with an intuitive meaning of the words and then work our way to a more consolidated picture of the complete phrase.

proof of program correctness: the program behaves as it was intended to behave
This clever "intuitive meaning" gives rise to a whole lot of questions. What do you mean by "program behaves" ? How do you measure that ? What do you mean by "intended to behave" ? How do you quantify that ? And finally, how do you prove the following equality ? :
program behaves =??= intended to behave

We are in for some serious and interesting debate on all these questions. Fasten your seat belts, get ready for a fascinating journey.

 

About the title :

The title of this CDROM -- The burden of proof is a phrase borrowed from legal language. In many countries, the onus or responsibility of proving that a person is guilty is on the one who accuses the person. In our case, the roles are reversed. The developer of automation systems is usually held rsponsible for proving that indeed his system or product is safe. This is a tough and challenging burden. Not only should he develop the system, he should also prove that the system will indeed behave like what the specifications said. Occasionally, this also leads to the developer finding out flaws in the specification itself. The naive end-user expects the developer to have taken the care of finding out flaws in the specification . The end user expects the system to behave without any of the undesired phenomena he has in mind (but has not made explicit in the specifications). In addition to all this, the developer is always under the threat of painful legal action, should any mishap occur later in the life cycle of the product he has delivered. That is why we think that proof is a major burden and have chosen this title for our CDROM.

Foundations and background | Logic | The lighter side of proof | Literature references

 

Background and foundations

GO TO TOP AND START AGAIN ^
 

The lighter side

there is always a brighter way to look at the gloomiest of things
GO TO TOP AND START AGAIN ^
 

Dangerously logical ? Or, logically dangerous ?

A quick look at the perils of bad logic.
GO TO TOP AND START AGAIN ^

Sections likely to be added soon ....


Differently similar

Approach to proof

Proof by induction
Proof by counter-example
Proof by
Model checking approach
theorem provin approach
Legal hurdles (I initiated a long discussion on this, in the safety critical mailing list. Here is a summary with added material from me.)

    

This is just a proof-of-concept CD

This CDROM has hyperlinks to a very large number of external sites. We have no control over the owners of these web sites. When we included these links, we visited every one of these sites. We also keep visiting these sites randomly. This CDROM is continuously updated on the basis of our experiences. Yet, some flaws may persist. If you find dead links, factual errors, or inappropriate contents, please exhibit some social responsibility please inform the author immediately, so that the next version of this CDROM does not carry forward these flaws.
no-gimmicks frame-free
TIDY OK-HTML4 OK-CSS 		ADMINISTRIVIA
 
Page last modified on: 2004-01-21
URL : (localpath)/top-page.htm
Send your comments, to: drpartha@gmail.com
Page developed by: Algologic Research & Solutions
Do not miss : Our Warning and Disclaimer page.
Simplicity is divine.
E W Dijkstra (1930-2002)

Go-to-top and start all over again ^