A Corrected Failure Divergence Model for CSP in Isabelle/HOL
作者： H. Tej , B. Wolff
关键词: Divergence (computer science) 、 Functional programming 、 Symbol (formal) 、 Mathematics 、 Higher-order logic 、 Formal representation 、 Automated theorem proving 、 HOL 、 Discrete mathematics 、 Denotational semantics
摘要: We present a failure-divergence model for CSP following the concepts of [BR 85]. Its formal representation within higher order logic in theorem prover Isabelle/HOL [Pau 94] revealed an error basic definition concerning treatment termination symbol tick.
core.ac.uk
springer.com
sci-hub.st 参考文章(10)
Albert J. Camilleri, A Higher Order Logic Mechanization of the CSP Failure-Divergence Semantics Springer, London. pp. 123- 150 ,(1991) , 10.1007/978-1-4471-3182-3_9
Kolyang, T. Santen, B. Wolff, Correct and User-Friendly Implementations of Transformation Systems formal methods. pp. 629- 648 ,(1996) , 10.1007/3-540-60973-3_111
M. J. C. Gordon, T. F. Melham, Introduction to HOL: a theorem proving environment for higher order logic Cambridge University Press. ,(1993)
Jonathan P. Bowen, Michael G. Hinchey, Seven more myths of formal methods: Dispelling industrial prejudices formal methods. pp. 105- 117 ,(1994) , 10.1007/3-540-58555-9_91
S. D. Brookes, A. W. Roscoe, An Improved Failures Model for Communicating Processes international conference on concurrency theory. pp. 281- 305 ,(1984) , 10.1007/3-540-15670-4_14
Tobias Nipkow, Lawrence C. Paulson, Isabelle: A Generic Theorem Prover ,(1994)
Kolyang, T. Santen, B. Wolff, A structure preserving encoding of Z in isabelle/HOL Lecture Notes in Computer Science. pp. 283- 298 ,(1996) , 10.1007/BFB0105411
Alonzo Church, A Formulation of the Simple Theory of Types Journal of Symbolic Logic. ,vol. 5, pp. 56- 68 ,(1940) , 10.2307/2266170
Peter B. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof ,(2002)
A. W. Roscoe, Geoff Barrett, Unbounded Nondeterminism in CSP international conference on mathematical foundations of programming semantics. pp. 160- 193 ,(1989) , 10.1007/BFB0040257