(* File: PAC_Checker_Specification.thy Author: Mathias Fleury, Daniela Kaufmann, JKU Maintainer: Mathias Fleury, JKU *) theory PAC_Checker_Specification imports PAC_Specification Refine_Imperative_HOL.IICF Finite_Map_Multiset begin section ‹Checker Algorithm› text ‹ In this level of refinement, we define the first level of the implementation of the checker, both with the specification as on ideals and the first version of the loop. › subsection ‹Specification›