Eiffel is a pure, statically typed OO language. It has built-in support for Design By Contract (DbC). DbC allows specifiaction to be taught as part of foundational computational thinking at the university level. Students who learn the benefits of principled thinking and see the value of the related tools will retain these lessons throughout their careers. Eiffel is an industrial strength object-oriented language that has influenced other languages such as Java, C# and UML. Companies use Eiffel because it provides the right paradigms to address the construction of large, high-quality object oriented software systems. Eiffel is more than a language; it is a framework for thinking about, specifying, designing and implementing object-oriented software.

http://eiffel.eecs.yorku.ca

PVS (Prototype Verification System) is a specification language and theorem prover for validating specifications. PVS helps engineers to design coherent specifications, and to predict the behaviour of systems satisfying the specifications — before implementing them. PVS provides interactive assistance to prove theorems that validate the specifications/models. PVS has been used by OPG to certify nuclear reactors, by NASA for space/avionic systems, and in a large number of other mission critical applications. PVS is both a language and an inference system. The language is a typed higher order logic, featuring undecidable type checking. You cannot write code (such as Java, Ruby or Haskell). You can only write mathematics. It thus forces one to write specifications of systems (i.e. what systems do free of implementation detail) and not how they do it. Furthermore, PVS can so some automatic syntax, typing and other checks that helps ensure that specifications are meaningful. PVS can then be used to validate the specifications. For example, if you have specified what it is to reverse a list, then you should be able to prove that if you reverse the list again you get the original list.

http://pvs.eecs.yorku.ca