private WyalFile . VariableDeclaration [ ] generatePostconditionTypePattern ( WyilFile . Decl . FunctionOrMethod declaration , LocalEnvironment environment ) { Tuple < Decl . Variable > params = declaration . getParameters ( ) ; Tuple < Decl . Variable > returns = declaration . getReturns ( ) ; WyalFile . VariableDeclaration [ ] vars = new WyalFile . VariableDeclaration [ params . size ( ) + returns . size ( ) ] ; // second, set initial environment for ( int i = 0 ; i != params . size ( ) ; ++ i ) { WyilFile . Decl . Variable var = params . get ( i ) ; vars [ i ] = environment . read ( var ) ; } for ( int i = 0 ; i != returns . size ( ) ; ++ i ) { WyilFile . Decl . Variable var = returns . get ( i ) ; vars [ i + params . size ( ) ] = environment . read ( var ) ; } // return vars ; }
Convert the return types for a given function or method declaration into a corresponding list of type patterns . This is primarily useful for generating declarations from functions or method .