public WyalFile . Stmt . Block buildVerificationCondition ( WyilFile . Decl declaration , GlobalEnvironment environment , VerificationCondition vc ) { WyalFile . Stmt antecedent = flatten ( vc . antecedent ) ; Expr consequent = vc . consequent ; HashSet < WyalFile . VariableDeclaration > freeVariables = new HashSet <> ( ) ; freeVariables ( antecedent , freeVariables ) ; freeVariables ( consequent , freeVariables ) ; // Determine any variable aliases as necessary. Expr aliases = determineVariableAliases ( environment , freeVariables ) ; // Construct the initial condition WyalFile . Stmt verificationCondition = implies ( and ( aliases , antecedent ) , vc . consequent ) ; // Now, generate type information for any free variables if ( freeVariables . size ( ) > 0 ) { // This indicates there are one or more free variables in the // verification condition. Hence, these must be universally // quantified to ensure the vc is well=typed. WyalFile . VariableDeclaration [ ] parameters = freeVariables . toArray ( new WyalFile . VariableDeclaration [ freeVariables . size ( ) ] ) ; WyalFile . Stmt . Block qfBody = new WyalFile . Stmt . Block ( verificationCondition ) ; verificationCondition = new WyalFile . Stmt . UniversalQuantifier ( parameters , qfBody ) ; } // Done return new WyalFile . Stmt . Block ( verificationCondition ) ; }
Construct a fully typed and quantified expression for representing a verification condition . Aside from flattening the various components it must also determine appropriate variable types including those for aliased variables .