Anzeige
Erschienen in:
2007 | OriginalPaper | Buchkapitel
Specifying and Verifying Programs in Spec#
verfasst von : K. Rustan M. Leino
Erschienen in: Perspectives of Systems Informatics
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Spec# is research programming system that aims to provide programmers with a higher degree of rigor than in common languages today. The Spec# language extends the object-oriented .NET language C#, adding features like non-null types, pre- and postconditions, and object invariants. The language has been designed to support an incremental path to using more specifications. Some of the new features of Spec# are checked by a static type checker, some give rise to compiler-emitted run-time checks, and all can be subjected to the Spec# static program verifier. The program verifier generates verification conditions from Spec# programs and then uses an automatic theorem prover to analyze these.