2
$\begingroup$

So it seems that you can get pretty far with just type definitions as a formal model of a system. The typed properties verify that the properties will have that type, typed function arguments verify the functions will get the appropriate input and output types, etc.

But now I am wondering about algorithms. In an ideal world an algorithm would just be a typed object as well and the algorithm's correctness would be inherent in the type definitions. I can't see how that would be possible, so I resort back to my brief readings of proving algorithms. Essentially you want to have an assertion before and after any loop, to establish a loop invariant. This way you can reason through induction that every step of the algorithm works as expected.

I am just not sure what I want to prove in the first place. I would like to have my code be:

  1. Robust.
  2. Fault tolerant.
  3. Fast.
  4. Bug-free.
  5. Scalable.
  6. All the things you would typically want.

So I define a specification for the algorithm:

  • The algorithm should return a type x object (types handle it automatically).
  • The algorithm should ~~ chug through the elements one at a time and compute a sum (lets say) ~~. That's where it starts to get fuzzy. Wondering if this is where the "loop invariant" comes in.
  • If there are no loops or branching in the algorithm (but maybe if-statements), then I want to prove (or "validate") that the value falls within some set of acceptable values.
  • etc.

So it seems that the quality of the application is dependent on how well-specified the behavior is. If you miss edge-cases, there will be bugs. If you don't specify the acceptable output values of the function, then you may get XSS. Wondering if that is a correct assessment, that everything revolves around the specification. Without that, there is nothing to prove.

Then it seems that you need to do testing first, in order to even comprehend the types of things you want to prove to be correct. It's like you start with some unit tests, and slowly evolve it to proofs. Wondering if that is a correct assessment. Once you know all the inputs and outputs of the algorithm through some thorough testing, then you can write some sort of proof that the algorithm is correct and avoids the error cases. This just seems like a really good unit test.

To summarize, it seems like what you want to prove with algorithms is that they are correct with regards to a specification. And the specification is a living document that you can start out with by writing unit tests which slowly evolve into proofs (somehow).

Just looking for some pointers on if I am on the right track, and how to know what to prove in an algorithm.

Improve this question
$\endgroup$
5
  • 1
    $\begingroup$ "what you want to prove with algorithms is that they are correct with regards to a specification" -- exactly. For clean problems like "sort a list of integers", it's usually easy to express an exact specification (e.g., "the output array $y_1, \dots, y_n$ should contain the same multiset of integers as the input array $x_1, \dots, x_n$, and should additionally obey $y_1 \le y_2 \le \dots \le y_n$"). Many real-world problems are much less clean, so are harder to develop accurate specifications for. $\endgroup$
    – j_random_hacker
    Commented Jun 21, 2018 at 10:27
  • $\begingroup$ That deals with correctness (your item 4). Item 3 is also commonly dealt with by proving (usually worst-case) upper bounds on the asymptotic complexity of the algorithm. Certain formalisations of items 1 and 2 can sometimes also be proven formally (e.g., it may be possible to prove that a set of interacting processes will never deadlock). Something that should never be part of a specification is how the algorithm should accomplish something ("chugging through one element at a time") -- this would force us to conclude that an algorithm that adds numbers in some other order is incorrect! $\endgroup$
    – j_random_hacker
    Commented Jun 21, 2018 at 10:42
  • $\begingroup$ The specifications of the algorithm are defined by you. So, when you prove things, you prove it w.r.t. to the specs you give. But, the specs might not be what you want. $\endgroup$
    – xuq01
    Commented Jun 21, 2018 at 16:23
  • $\begingroup$ Obviously, correctness is the most important criteria. When people write certified software (i.e. mathematically proved correct code) thr first thing they go for is correctness. Then they come up with other desirable qualities and prove them. But then, nothing is perfect, and how much do you care to prove is about you. $\endgroup$
    – xuq01
    Commented Jun 21, 2018 at 16:24
  • $\begingroup$ For example, a typical specification for merge sort for FM people might be that it (1) returns the same elements as the original list and (2) is in ascending order. However, people usually do not care to prove things about its time complexity but that is obviously also important; many people don't do it because they perceive that it is not worth it. $\endgroup$
    – xuq01
    Commented Jun 21, 2018 at 16:27

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.