Translating Spec# Programs to C# with CodeContracts
Florian Egli · Repository for Publications and Research Data (ETH Zurich) · 2012
Contracts are used to specify the behavior of programs.These contracts can be verified statically, to prove that the program code is correct and the contracts are always satisfied, or they can be asserted during runtime.One programming language that offers support for contracts is Spec # .It implements an ownership model to ensure code correctness.Spec # tool support is limited to sscBoogie for static verification.CodeContracts is a project that aims to offer contracts for standard .Net, with a different specification language than Spec # and extended tool support.The goal of this thesis is to design an encoding for Spec # programs in C # and CodeContracts.With this, we are able to translate programs written in Spec # to CodeContracts compatible code, extended with ownership states and assertions that would be checked by sscBoogie, while preserving the programs semantic.For the translation, we use an extension of CodeContracts, that provides additional specification constructs, called CodeContracts++.These translated programs can then be analyzed and tested with tools that support CodeContracts, such as Pex for automatic test generation and Clousot for code analysis, that otherwise would not be available for Spec # .// t h i s .k e y u p d a t ef r a m e c o n d i t i o n C o n t r a c t .A s s e r t ( t h i s != n u l l , "F i e l d o w n e r o f f i e l d ' key ' i s n u l l .") ; C o n t r a c t .A s s e r t ( t h i s .I s W r i t a b l e ( ) , "F i e l d o w n e r o f f i e l d ' key ' i s n o t w r i t a b l e ") ; G h o s t V a r i a b l e > S S g f 0 = new G h o s t V a r i a b l e >( F i e l d .C r e a t e ( t h i s , "Node .k e y ") , " A s s i g n e d F i e l d ") ; C o n t r a c t .A s s e r t ( CCSS .I s F i e l d M o d i f i a b l e ( ˜S S g f 0 , ˜S S m o d i f i a b l e F i e l d s , ˜S S m o d i f i a b l e O b j e c t s , ( I S e t )˜S S f r e s h ) , " F i e l d ' key ' i s n o t m o d i f i a b l e .") ; t h i s .k e y = k e y ; C o n t r a c t .A s s e r t ( t h i s .I s M u t a b l e ( t y p e o f ( Node ) ) | | t h i s .S S I n v ( ) , "F i e l d o w n e r o f f i e l d ' key ' i s n o t m u t a b l e o r i n v a r i a n t d o e s n o t h o l d .") ; // t h i s .v a l u p d a t ef r a m e c o n d i t i o n C o n t r a c t .A s s e r t ( t h i s != n u l l , "F i e l d o w n e r o f f i e l d ' v a l ' i s n u l l .") ; C o n t r a c t .A s s e r t ( t h i s .I s W r i t a b l e ( ) , "F i e l d o w n e r o f f i e l d ' v a l ' i s n o t w r i t a b l e ") ; G h o s t V a r i a b l e > S S g f 1 = new G h o s t V a r i a b l e >( F i e l d .C r e a t e ( t h i s , "Node .v a l ") , " A s s i g n e d F i e l d ") ; C o n t r a c t .A s s e r t ( CCSS .I s F i e l d M o d i f i a b l e ( ˜S S g f 1 , ˜S S m o d i f i a b l e F i e l d s , ˜S S m o d i f i a b l e O b j e c t s , ( I S e t )˜S S f r e s h ) , " F i e l d ' v a l ' i s n o t m o d i f i a b l e .") ; t h i s .v a l = v a l ; C o n t r a c t .A s s e r t ( t h i s .I s M u t a b l e ( t y p e o f ( Node ) ) | | t h i s .S S I n v ( ) , "F i e l d o w n e r o f f i e l d ' v a l ' i s n o t m u t a b l e o r i n v a r i a n t d o e s n o t h o l d .") ; // E s t a b l i s h p o s t c o n d i t i o n C o n t r a c t .A s s e r t ( t h i s .S S I n v ( ) , "O b j e c t i n v a r i a n t o f o b j e c t ' Node t h i s ' d o e s n o t h o l d .") ; t h i s .A d d i t i v e P a c k ( t y p e o f ( Node ) ) ;