private void translateTypeDeclaration ( WyilFile . Decl . Type declaration ) { WyilFile . Tuple < WyilFile . Expr > invariants = declaration . getInvariant ( ) ; WyalFile . Stmt . Block [ ] invariant = new WyalFile . Stmt . Block [ invariants . size ( ) ] ; WyalFile . Type type = convert ( declaration . getType ( ) , declaration ) ; WyalFile . VariableDeclaration var ; if ( invariants . size ( ) > 0 ) { WyilFile . Decl . Variable v = declaration . getVariableDeclaration ( ) ; // First, translate the invariant (if applicable) GlobalEnvironment globalEnvironment = new GlobalEnvironment ( declaration ) ; LocalEnvironment localEnvironment = new LocalEnvironment ( globalEnvironment ) ; var = localEnvironment . read ( v ) ; for ( int i = 0 ; i != invariant . length ; ++ i ) { invariant [ i ] = translateAsBlock ( invariants . get ( i ) , localEnvironment ) ; } } else { var = new WyalFile . VariableDeclaration ( type , new WyalFile . Identifier ( "self" ) ) ; } // Done Name name = declaration . getQualifiedName ( ) . toName ( ) ; WyalFile . Declaration td = new WyalFile . Declaration . Named . Type ( name , var , invariant ) ; allocate ( td , declaration . getParent ( WyilFile . Attribute . Span . class ) ) ; }
Transform a type declaration into verification conditions as necessary . In particular the type should be inhabitable . This means for example that the invariant does not contradict itself . Furthermore we need to translate the type invariant into a macro block .