Modelling and analysing data dependencies and consistency between classes and objects is a complex task. We show that dependently typed programming languages can handle this in a particularly simple, convenient and highly automated way. Dependent datatypes are used to implement (meta)models for classes and objects directly and concisely. Data dependencies and similar system constraints are specified within the language's expressive type system. Verification and propagation of these constraints is handled by type inference, which can be enhanced by customised decision procedures or external solvers if needed. The approach thus supports the development of software models that are correct by construction. © 2012 Springer-Verlag.
CITATION STYLE
Foster, S., Rypáček, O., & Struth, G. (2012). Correctness of object oriented models by extended type inference. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7521 LNCS, pp. 46–60). https://doi.org/10.1007/978-3-642-32943-2_4
Mendeley helps you to discover research relevant for your work.