An `Executable' Impredicative Semantics for the Ada Configuration.