private void translateConstantDeclaration ( WyilFile . Decl . StaticVariable decl ) { if ( decl . hasInitialiser ( ) ) { // The environments are needed to prevent clashes between variable // versions across verification conditions, and also to type variables // used in verification conditions. GlobalEnvironment globalEnvironment = new GlobalEnvironment ( decl ) ; LocalEnvironment localEnvironment = new LocalEnvironment ( globalEnvironment ) ; List < VerificationCondition > vcs = new ArrayList <> ( ) ; Context context = new Context ( wyalFile , AssumptionSet . ROOT , localEnvironment , localEnvironment , null , vcs ) ; // Pair < Expr , Context > rp = translateExpressionWithChecks ( decl . getInitialiser ( ) , null , context ) ; generateTypeInvariantCheck ( decl . getType ( ) , rp . first ( ) , context ) ; // Translate each generated verification condition into an assertion in // the underlying WyalFile. createAssertions ( decl , vcs , globalEnvironment ) ; } }
Translate a constant declaration into WyAL . At the moment this does nothing because constant declarations are not supported in WyAL files .