I developed a specifications language. Depending on the comments on this, I’ll call it a "code-aware specifications language" or a "verification-aware specifications language". The idea I’m playing with is the gap between a programming language like C and a verification language like Dafny or Coq.

Problem statement: I have some RTOS code written in C and we need to verify properties like liveness and correctness. I have previously used Dafny to prove these properties with quite some success. I read the spec, implemented the required functions in Dafny, and then proved the liveness and correctness properties of an industrial RTOS. However, my Ph.D. advisor asked: "how can you show that your Dafny code is an exact representation of the C code that you're trying to verify?"

That is a valid question. In fact, the syntax and the semantics of C and Dafny have fundamental differences. To motivate that the Dafny implementation is, in fact, an exact representation of the underlying C program, a lot of hand-waving and baseless arguments were made that left my Ph.D. advisor even more unconvinced. He doesn't question the veracity of the Dafny implementation and in fact encourages to explore Dafny to it's depths but his question keeps bugging us both. A similar question arose when a colleague proved similar properties using UPPAAL, a formal modeling tool.

To answer his question, I came up with an idea of an intermediate specification language. This is not a new idea, though. Specification languages such as EventB, TLA+, etc. already exist. But the problem is a syntactic as well as a semantic disconnect between the specifications written in, for instance, EventB and the implementation written in C. Yes, there is a process of refinements that will lead one to an actual implementation but it requires expertise and a lot of work to actually get to the ground truth of the implementation.

My specification language is abstract enough to ignore, for instance, memory layouts, but concrete enough to reason about the implementation in a bit-precise manner. The language features specifications of concrete pre-conditions, program code, data structures, and the expected postconditions. The backend then verifies if, given the pre-condtions and the program code, the expected postconditions are satisfied. This gives one a "golden model". The specification language I developed implements the 8, 16, 32, and 64-bit unsigned integers in the same manner like C. There are integer indexed arrays or "sequences" as well as the idea of abstract uninterpreted functions. The grammar is quite simplistic but powerful enough to express complex logic. The best thing is the syntactic and visual similarity to C. Although I cannot formally prove the isomorphism between a given C program and the program written in my language, the visual and semantical similarity is quite convincing. An example follows:

%% declarations
// Declare all variables as uint32
const x: uint32;
const y: uint32;
z: uint32;
xc: uint32;
yc: uint32;
rc: uint32;
t1: uint32;
t2: uint32;
Azc: uint32;
zc: uint32;
const A: uint32;
const MAGIC: uint32;
Bx: uint32;
By: uint32;
Bz: uint32;
D: uint32;
failed: bool;
%% initialisation
%% preconditions
A == 32423;
MAGIC == 35622353255;
(MAGIC * A) == 1;
// Bx, By, Bz range
Bx > 0;
Bx < A; // This check is now also uint32
By > 0;
By < A;
Bz > 0;
Bz < A;
x > 0;
x < 65536;
y > 0;
y < 65536;
x * y < 65536;
D > 0;
xc == (A * x + Bx + D);
yc == (A * y + By + D);
failed == false;
%% postconditions
// These are now bit-vector operations
zc == (A * (x * y) + Bz + D);
(failed == false) => ((z / A) == (x * y));
z % A == 0;
%% program
// All math is now implicitly 32-bit bit-vector math
rc := (xc * yc);
t1 := (((By + D) * xc) + ((Bx + D) * yc) - (Bx * By) - (Bz * A));
t2 := (((Bx + By + A) * D) + (D * D));
Azc := (rc - t1 + t2);
zc := (MAGIC * Azc);
z := (zc - Bz - D);
if((z / A) != (x * y))
{
 failed := true;
}

A uint32 is the same as an unsigned 32-bit integer in C. The code above is the specification of whatever this function does. The backend tries to verify that, given the program (in the %% program section) and the pre-conditions (given in the %% preconditions section), the postconditions (%% postconditions) are satisfied. Without any effort, a given C implementation of this program can be shown to be "isomorphic" to this specification. If the spec are not verified, i.e., the postconditions are not satisfied, then the C program is also not correct.

So now, the question is: how is this approach different from, for instance, EventB? Is this approach even valid? Is such a specification language useful? Sorry for the long question and any comments and help is appreciated!