Databases
StackOverflow2013
Postsdbo
PO
 

Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    primarykey
    data
    text
    <p>Usually proofs of correctness are very specific to the algorithm at hand.</p> <p>However, there are several well known tricks that are used and re-used again. For example, with recursive algorithms you can use <a href="http://en.wikipedia.org/wiki/Loop_invariant" rel="nofollow noreferrer">loop invariants</a>.</p> <p>Another common trick is reducing the original problem to a problem for which your algorithm's proof of correctness is easier to show, then either generalizing the easier problem or showing that the easier problem can be translated to a solution to the original problem. <a href="http://en.wikipedia.org/wiki/Reduction_%28complexity%29" rel="nofollow noreferrer">Here</a> is a description.</p> <p>If you have a particular algorithm in mind, you may do better in asking how to construct a proof for that algorithm rather than a general answer. </p>
    singulars
    1. This table or related slice is empty.
    1. POFormally verifying the correctness of an algorithm
      singulars
      1. PTQuestion
    1. PTAnswer
    1. This table or related slice is empty.
    1. USldog
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    2. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    1. COAlgorithm reduction (especially described as in the link you offer) is a theoretical tool to demonstrate that a problem is at least as hard as another. These proofs, often done in the Turing machine computation model, are hand-wavy affairs and nothing like formal (machine-checkable) proofs. They are often done for problems to hard to be useful in practice (the example in your link is for the Halting problem; showing a problem is NP-hard by reducing a known NP-hard problem to it is also popular). In short, I'm not sure problem reduction, as linked, has anything to do with formal correctness.
      singulars
      1. PO
      1. USPascal Cuoq
    2. COHmm maybe reduction is not the correct term I should be using here. When I say reduction I meant something along the lines of the following example. Suppose that you have an algorithm that computes the intersection of N rectangles, which you know is correct. Suppose you have another problem for which there exists a non-trivial translation of that problem to the problem of computing the intersection of N rectangles. Then you use the first algorithm to compute the solution to the latter problem. All that remains is showing that the translation is correct.
      singulars
      1. PO
      1. USldog
    3. COBut I can see that this is confusing, its a trick that relies on the fact that you make use of a well known algorithm that is known to be correct (in this case the one to compute the intersection of N rectangels.) I can see where the confusion comes as to whether this is a method of proving or providing a correct algorithm.
      singulars
      1. PO
      1. USldog
 

Querying!

 
Guidance
A row detail

Detail views are divided into sections. All the information in the data section comes from columns in the selected row. The other sections display data from other, related rows.

Related data can be related in a to-one or a to-many fashion. Captions of data related in a to-many fashion link to a list view showing a filtered view of the table.

Try moving around until you find a non-empty to-many entry and click on the label to get to one. You can move back to the root by clicking on the database name in the header.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload