Static Program Verification and Proofs - Correct-by-Construction

[sirinath]

Is it possible to take a step beyond type checking and add program verification and proofs like that is found in WhyML, Dafny and Ada SPARK 2014?

Following is a WhyML example:

module MaxAndSum

  use import int.Int
  use import ref.Ref
  use import array.Array

  let max_sum (a: array int) (n: int)
    requires { 0 <= n = length a }
    requires { forall i:int. 0 <= i < n -> a[i] >= 0 }
    returns  { sum, max -> sum <= n * max }
  = let sum = ref 0 in
    let max = ref 0 in
    for i = 0 to n - 1 do
      invariant { !sum <= i * !max }
      if !max < a[i] then max := a[i];
      sum := !sum + a[i]
    done;
    (!sum, !max)

end

The key is we can have specifications like:

requires { 0 <= n = length a }
requires { forall i:int. 0 <= i < n -> a[i] >= 0 }
returns  { sum, max -> sum <= n * max }

and

invariant { !sum <= i * !max }

[JSMonk]

Sorry, but it's not a goal of the Hegel project. At this moment, we try to implement a strong type system with high-level type inference. Maybe in the future, we will add dependent types, but it's so far from really program verification. Thank you for your question ^_^.

[sirinath]

This might be of interest: Dependent Types for JavaScript