Comment by gtutino

That's basically SPARK (the Ada subset) but with c-like syntax (more or less).