Formal Algorithm Validation

Question

Firstly, is this only possible for algorithms that do not have side effects?

Secondly, where can I find out about this process, about any good books, articles, etc.

Answer 1

COQ is a validation assistant that produces the correct ocaml output. This is pretty tricky. I never thought it over, but my colleague started and then stopped using it after two months. This was mainly because he wanted to do everything faster, but if you need to test the algorithm, this might be a good idea.

Here is a course that uses COQ and talks about evidence-based algorithms.
And here is a tutorial about writing scientific articles in COQ.

Answer 2

• As a rule, it is much easier to check / prove the correctness when no side effects are involved, but this is not an absolute requirement.
• You might want to read some documents for a formal specification language, such as Z. A formal specification is not evidence itself, but often is the basis for it.

Answer 3

Usually proofs of correctness are very specific to the algorithm.

However, there are several well-known tricks that are used and reused again. For example, using recursive algorithms you can use loop invariants .

Another common trick is to reduce the original problem to a problem for which your algorithm has proven correct, easier to show, then either generalizing the easier problem or showing that the easier problem can be resolved to solve the original problem. Here is a description.

If you have a specific algorithm, you might better ask how to build a proof for this algorithm, rather than a general answer.

Answer 4

I believe that checking the correctness of the algorithm will confirm its compliance with the specification. There is a branch of theoretical computer science called Formal Methods , which may be what you are looking for if you need to get closer to the proof as you can. From Wikipedia

Formal methods are a special kind of mathematical methods for specification, development and verification of system software and hardware.

You can find many training resources and tools from a variety of links on the related Wikipedia page and from the Formical Methods wiki .

Answer 5

Buy these books: http://www.amazon.com/Science-Programming-Monographs-Computer/dp/0387964800

p>

Grish's book, scientific programming - great job. Patient, complete, complete.

Answer 6

Logic in computer science, Hoot and Ryan, provides a fairly readable overview of modern systems to test systems. Once upon a time, people talked about the correct verification of programs - with programming languages ​​that may or may not have side effects. The impression I get from this book elsewhere is that the real applications are different - for example, proving the protocol is correct or that the chip's floating-point block can be divided correctly or that the blocking function for managing linked lists is correct.

ACM Computing Surveys Vol 41 Issue 4 (October 2009) is a particular software validation issue. It looks like you can get at least one of the articles without an ACM account by looking for “Formal Techniques: Practice and Experience”.

Answer 7

The Frama-C tool, for which Elazar offers a demo video in the comments, gives you the specification language, ACSL , for writing function contracts and various analyzers to verify that the C function satisfies its contract and security conditions, such as no runtime errors.

An extended tutorial, ACSL, by example , shows examples of actual C-algorithms that are indicated and verified, and separates functions from effective ones without side effects (without side effects they are considered easier and come first in the textbook). This document is also interesting in that it was not written by the developers of the tools that it describes, so it provides a more recent and more didactic look at these methods.

Answer 8

If you are familiar with LISP, then you definitely need to check ACL2: http://www.cs.utexas.edu/~moore/acl2/acl2-doc.html

Answer 9

Dijkstra The discipline of programming and its EWD form the basis of formal testing as a science in programming. A simpler job - Wirth Systematic programming , which begins with a simple approach to using validation. Wirth uses pre-ISO Pascal for the language; Dijkstra uses a formalism similar to Algol 68 called Guarded (GCL). A formal check has ripened since Dijkstra and Hoar, but these old texts can still be a good starting point.

Answer 10

The PVS tool, developed by the Stanford guys, is a specification and verification system. I worked on this and found it very useful for theoretical proof.

Answer 11

WRT (1), you may have to create an algorithm model in such a way as to “capture” the side effects of the algorithm in a program variable designed to model such side effects based on state.