Clark and Tärnlud⁴ have proposed a methodology for the specification, desing and verification of logic programs in the framework of first order logic. Their main idea is to derive the correctness of a logic program from its own clauses and suitable induction axioma on the data. This approach has been also advocated by Cartwright³ for the case of recursive, functional programs. He has contributed some theoretical results about the semantics of programs in nonstandard structures, using the notion of least definable fixpoint of the operator naturally associated to a given recursive program: This idea is also implicit in the independent work of Andréka, Németi and Sain¹ and Hajék⁷ about nonstandard dynamic logic for flowchart-like programs and regular programs; see also Sain¹⁰.