A contract language for modular specification and verification of temporal properties
Deductive software verification is used to prove correctness of programs with respect to contracts. Contracts are commonly expressed on procedures of a program using Hoare logic. Such contracts consist of a precondition, specifying a condition that must hold before the procedure is executed, and a p...
| Main Author: | |
|---|---|
| Format: | Others |
| Language: | English |
| Published: |
KTH, Skolan för elektroteknik och datavetenskap (EECS)
2020
|
| Subjects: | |
| Online Access: | http://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-280457 |