Correctness of object oriented models by extended type inference
作者： Simon Foster , Ondřej Rypáček , Georg Struth
DOI: 10.1007/978-3-642-32943-2_4
关键词:
摘要: Modelling and analysing data dependencies consistency between classes objects is a complex task. We show that dependently typed programming languages can handle this in particularly simple, convenient highly automated way. Dependent datatypes are used to implement (meta)models for directly concisely. Data similar system constraints specified within the language's expressive type system. Verification propagation of these handled by inference, which be enhanced customised decision procedures or external solvers if needed. The approach thus supports development software models correct construction.
springer.com
sci-hub.st 参考文章(18)
Stephan Merz, Alexander Knapp, Model Checking and Code Generation for UML State Machines and Collaborations ,(2002)
Graeme Smith, Florian Kammüller, Thomas Santen, Encoding Object-Z in Isabelle/HOL Lecture Notes in Computer Science. pp. 82- 99 ,(2002) , 10.1007/3-540-45648-1_5
Yves Bertot, Pierre Casteran, Interactive Theorem Proving and Program Development ,(2004)
Ana Bove, Peter Dybjer, Ulf Norell, A Brief Overview of Agda --- A Functional Language with Dependent Types theorem proving in higher order logics. ,vol. 5674, pp. 73- 78 ,(2009) , 10.1007/978-3-642-03359-9_6
Iman Poernomo, Proofs-as-Model-Transformations international conference on model transformation. pp. 214- 228 ,(2008) , 10.1007/978-3-540-69927-9_15
David Aspinall, Jaroslav Ševčík, Formalising java's data race free guarantee theorem proving in higher order logics. pp. 22- 37 ,(2007) , 10.1007/978-3-540-74591-4_4
Simon Foster, Georg Struth, Integrating an automated theorem prover into agda nasa formal methods. pp. 116- 130 ,(2011) , 10.1007/978-3-642-20398-5_10
Achim D. Brucker, Burkhart Wolff, HOL-OCL: Experiences, Consequences and Design Choices Lecture Notes in Computer Science. pp. 196- 211 ,(2002) , 10.1007/3-540-45800-X_17
Frédéric Jouault, Freddy Allilaire, Jean Bézivin, Ivan Kurtev, ATL: A model transformation tool Science of Computer Programming. ,vol. 72, pp. 31- 39 ,(2008) , 10.1016/J.SCICO.2007.08.002
Pierre-Alain Muller, Franck Fleurey, Jean-Marc Jézéquel, Weaving Executability into Object-Oriented Meta-languages Model Driven Engineering Languages and Systems. pp. 264- 278 ,(2005) , 10.1007/11557432_19