1

I'm looking for a programming language/tool that can do these two things:

  1. Prove that a program is correct, i.e. adheres to its specifications.
  2. Prove that a program will run in less than N seconds and/or perform less than N simple operations, for a bounded input size.

Example:

Given something like this code (with or without extra annotations, or even in a different programming language):

/*
guaranteed: n ≤ 100000
guaranteed: n ≥ 1
guaranteed: v ≤ 1000000000
guaranteed: v ≥ 1
guaranteed: forall 1 ≤ i ≤ n; a[i] ≥ 1
guaranteed: forall 1 ≤ i ≤ n; a[i] ≤ 1000000000
prove: performs less than 100 operations
prove: runs in less than 200 ms
returns: i such that a[i] = v, or -1 if forall 1 ≤ i ≤ n; a[i] ≠ v
*/
int binary_search(int* a, int n, int v) {
    int l = 0;
    int r = n - 1;
    while(l < r) {
        int m = (l + r) / 2;
        if(a[m] == v) return m;
        else if(a[m] < v) r = m - 1;
        else if(a[m] > v) l = m + 1;
    }
    return -1;
}

The language should return that all conditions hold.

2
  • The actual run time duration will, of course, depend on the hardware available so the best that you could hope for is the number of steps. – Steve Barnes May 7 '18 at 6:16
  • That is also acceptable. There are also WCET estimators I could use, but a high-level analysis of the cost is perfectly fine. – Mitsos101 May 7 '18 at 11:59
1

It appears that there are several ways to achieve this.

  1. A generic compiler + a worst case execution time (WCET) analyzer such as aiT could be used. This seems to be the only approach that provides an estimate of the runtime, and not of the runtime complexity. According to the aiT developers, this also takes into account the fact that the same instructions may be executed faster if rearranged. This is difficult to account for if the following methods are used. However, the estimates given do not seem to be formally provable.

  2. Another approach is the use of a dependently typed, formally provable programming language such as Coq, Agda, or Idris, and use the functional programming concept of monads to assign a cost to each simple operation, and sum all costs together. Implementations of this method can be seen here: Coq implementation, Agda implementation, Idris implementation. One might also find this blog post useful if this approach is to be implemented in a programming language other than the aforementioned.

  3. However, the approach that corresponds the closest to the example given in the question is the use of the specification language ACSL and the plugins in the Frama-C platform, which can be used to formally prove properties of programs written in C. Instead of a monad, a global variable that keeps track of the total cost is used. An implementation of this approach can be seen in the CerCo compiler (see also this paper). Nonetheless, the user may sometimes have to prove their assertions manually to obtain a tighter bound on the cost, which can be done through the use of the Coq programming language, which is mentioned in approach 2.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.