Abstrakt. Objektorienterade språk ger fördelar som återanvändning och modularitet, men de ger också nya utmaningar för programverifiering. Programlogik har utvecklats för språk som C# och Java. Dessa logiker täcker dock inte detaljerna i Eiffelspråket. Detta dokument presenterar en programlogik för Eiffel som hanterar undantag, en gång rutiner, och flera arv. Logiken är beprövad ljud och komplett w.r.t. En operationell semantik. Lärdomar om språkdesign som man lärt sig av erfarenheten diskuteras.
Arbetet i REF presenterar en Hoare-stil programlogik för Eiffel som hanterar flera arv baserat på en befintlig programlogik för single-arv genom att utöka metoden lookup definition.
A Sound and Complete Program Logic for Eiffel
{'venue': 'TOOLS', 'journal': None, 'mag_field_of_study': ['Computer Science']}