?. Xa-xb, ¬ xa < x ?? ¬ xb < x ?? xb < xa ?? [x , xb, xa] = PUT [xb, xa

X. Put, PO ((??X6X76 < ??X5X75 ? ¬ ??X7X77 < ??X5X75 ) ? ¬ ??X7X77 < ??X6X76 ) THYP ((? x xa xb, THYP (3 < length l ?? List-test.sort l = PUT l )]] =? (List-test

?. ]. , ?. , ?. Sut-[-?2, ?. , ?. et al., write-list) gdb-script:: writeFiles filePath fileExtension gdb-script-list, ?2 , ?1 , ?1 , 0 ] = SUT [?2 , ?1 , ?1 , ?2 , 0 ] [?2 , ?2 , ?1 , 0 , 0 ] = SUT [?2 , 0 , ?1 , ?2 , 0 ] [?1 , ?1 , 0 , 0 , 0 ] = SUT ([filePath] @ [(gdb-script :: gdb-script-list) |> length |> Int.toString] @ [fileExtension] |> String.concat |> Path.explode |> File, 2000.

M. Thy-load, master-directory @{theory}; fun masterPath-add theory Path = Path |> Path.explode |> Path.append (Thy-Load .master-directory theory) |> Path.implode

. Pretty, writeln (pretty-terms @{context}

P. B. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Bibliography Computer Science and Applied Mathematics, vol.27, 1986.
DOI : 10.1007/978-94-015-9934-4

S. Berghofer and T. Nipkow, Random testing in Isabelle/HOL, Proceedings of the Second International Conference on Software Engineering and Formal Methods, 2004. SEFM 2004., pp.230-239, 2004.
DOI : 10.1109/SEFM.2004.1347524
URL : http://www4.in.tum.de/~berghofe/papers/SEFM04.pdf

A. Biere, A. Cimatti, E. Clarke, O. Strichman, and Y. Zhu, Bounded Model Checking, Advances In Computers, 2003.
DOI : 10.1016/S0065-2458(03)58003-2

S. Böhme and T. Weber, Fast LCF-Style Proof Reconstruction for Z3, Interactive Theorem Proving (ITP), pp.179-194, 2010.
DOI : 10.1007/978-3-642-14052-5_14

A. D. Brucker, O. Havle, Y. Nemouchi, and B. Wolff, Testing the IPC Protocol for a Real-Time Operating System, Verified Software: Theories, Tools, and Experiments -7th International Conference, pp.40-60, 2015.
DOI : 10.1145/267580.267590
URL : https://hal.archives-ouvertes.fr/hal-01274698

A. D. Brucker and B. Wolff, Symbolic Test Case Generation for Primitive Recursive Functions, Formal Approaches to Testing of Software, number 3395 in Lecture Notes in Computer Science, pp.16-32, 2005.
DOI : 10.1145/267580.267590

A. D. Brucker and B. Wolff, A verification approach to applied system security, International Journal on Software Tools for Technology Transfer, vol.architecture, issue.3, 2005.
DOI : 10.1007/3-540-45853-0_12

A. D. Brucker and B. Wolff, hol-TestGen, Fundamental Approaches to Software Engineering (FASE09), number 5503 in Lecture Notes in Computer Science, pp.417-420, 2009.
DOI : 10.1016/j.entcs.2008.11.003
URL : https://hal.archives-ouvertes.fr/hal-01765526

A. D. Brucker and B. Wolff, On theorem prover-based testing. Formal Aspects of Computing, 2012.
DOI : 10.1007/s00165-012-0222-y
URL : http://www.brucker.ch//bibliography/download/2012/brucker.ea-theorem-prover-2012.pdf

A. Church, A formulation of the simple theory of types, The Journal of Symbolic Logic, vol.1, issue.02, pp.56-68, 1940.
DOI : 10.2307/2371199

K. Claessen and J. Hughes, QuickCheck: a lightweight tool for random testing of Haskell programs, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, pp.268-279, 2000.

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977.
DOI : 10.1145/512950.512973
URL : https://hal.archives-ouvertes.fr/hal-01108790

J. Dick and A. Faivre, Automating the generation and sequencing of test cases from model-based specications, Formal Methods Europe 93: Industrial-Strength Formal Methods, pp.268-284, 1993.

P. Dybjer, Q. Haiyan, and M. Takeyama, Verifying Haskell programs by combining testing and proving, Third International Conference on Quality Software, 2003. Proceedings., p.272, 2003.
DOI : 10.1109/QSIC.2003.1319111

M. Gaudel, Testing can be formal, too, TAPSOFT 95, pp.82-96, 1995.
DOI : 10.1007/3-540-59293-8_188

S. Hayashi, Towards the animation of proofs ??? testing proofs by examples, Theoretical Computer Science, vol.272, issue.1-2, pp.177-195, 2002.
DOI : 10.1016/S0304-3975(00)00350-9

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL ? A Proof Assistant for Higher-Order Logic, LNCS, vol.2283, 2002.

. Poly, ML ? the poly/ml implementation of standard ml

M. Wenzel, The Isabelle/Isar Reference Manual, 2004.

H. Zhu, P. A. Hall, and J. H. May, Software unit test coverage and adequacy, ACM Computing Surveys, vol.29, issue.4, pp.366-427, 1997.
DOI : 10.1145/267580.267590