[churnedgodotdev]

Ada solved these problems in 1983.

More recently, you can use Frama-C to constrain allowable sequences of 0's and 1's for C types and formally verify correctness.

In Ada since 1983 you can, e.g, declare your own 8 bit signed symmetric type without the wart -128 like so:

  type Sym_8 is new Integer range -127 .. 127;

Then this fails at compile time:

  My_Signed_Byte : Sym_8 := -128;
  

SPARK can prove all execution paths through your program are free of such constraint violations. This means safe SPARK code can disable runtime checks and run faster than the safest Rust/Zig dev settings, which insert runtime checks for over/under flow.

In Frama-C, say you want a function that returns an absolute value. This function will fail to verify:

  /*@ ensures (x >= 0 ==> \result == x) &&
              (x < 0 ==> \result == -x);
      assigns \nothing;  */
  int abs (int x) {
      if (x >=0)
          return x;
      return -x;
  }

It fails to verify because you might have x==INT_MIN. So this will verify:

  #include <limits.h>
  /*@ requires x > INT_MIN;
      ensures (x >= 0 ==> \result == x) &&
              (x < 0 ==> \result == -x);
      assigns \nothing;  */
  int abs (int x) {
      if (x >=0)
          return x;
      return -x;
  }

[KsassPeuk]

For the sake of completeness: Frama-C (+ WP plugin) can verify that the program conforms to the first specification, however, it indeed can't verify that the program does not contain an undefined behavior (reason why we write the second specification).

[Ygg2]

How does this work in presence of user supplied values?

It has to have a check somewhere, no?

[churnedgodotdev]

Of course. The checks are performed where the values arrive. If a file or network socket provides a number N that is going to be used as an array index, then N must be proved to be within array bounds at compile time before being used as an array index, which means you are forced to catch the bug at compile time and decide how to signal bad values of N.

[Ygg2]

Ok, but you can't check _runtime_ values at _compile_ time. If you have user input/file system/network supply N (where 0<N<100) you still HAVE to check it somewhere. You still have to have a runtime check when interacting with outside world.

[churnedgodotdev]

Of course, that's what I thought I said in my previous comment but I guess I wasn't crystal clear. The formal verification stack basically tells you, "There's no guarantee 0<N<100 holds if you get N from an I/O stream. N can be anything." So it's your job to insert a runtime check for N<=0 or N>=100 and decide how best to handle that, e.g. panic and quit, or clamp N to a valid range if it makes sense, or avoid accessing the array if it makes sense. But the system won't let you use a possibly out of range N as an array subscript so you are forced to code a solution to this special case "at compile time", typically by inserting a runtime check. Though if you are reading data from a trusted ROM you can also use a pragma or special assert to say, "This data can be trusted to have this invariant" and avoid the runtime check.