Type-Level Property Based Testing

被引：0
作者：
Hansen, Thomas Ekstrom [1 ]
Brady, Edwin [1 ]
机构：
[1] Univ St Andrews, Sch Comp Sci, St Andrews, Fife, Scotland
来源：
PROCEEDINGS OF THE 9TH ACM SIGPLAN INTERNATIONAL WORKSHOP ON TYPE-DRIVEN DEVELOPMENT, TYDE 2024 | 2024年
基金：
英国工程与自然科学研究理事会;
关键词：
property based testing; dependent types; state machines; software design;
D O I：
10.1145/3678000.3678206
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We present an automated framework for solidifying the cohesion between software specifications, their dependently typed models, and implementation at compile time. Model Checking and type checking are currently separate techniques for automatically verifying the correctness of programs. Using Property Based Testing (PBT), Indexed State Monads (ISMs), and dependent types, we are able to model several interesting systems and network protocols, have the type checker verify that our implementation behaves as specified, and test that our model matches the specification's semantics; a step towards combining model and type checking.
引用
收藏
页码：37 / 49
页数：13
相关论文
共 41 条
  • [1] Arts T, 2015, IEEE ICST WORKSHOP
  • [2] Syntax and Semantics of Quantitative Type Theory
    Atkey, Robert
    [J]. LICS'18: PROCEEDINGS OF THE 33RD ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, 2018, : 56 - 65
  • [3] Barwell AD, 2023, Arxiv, DOI [arXiv:2305.06238, 10.48550/arXiv.2305.06238, DOI 10.48550/ARXIV.2305.06238]
  • [4] Bengtsson J., 1996, Hybrid Systems III. Verification and Control, P232, DOI 10.1007/BFb0020949
  • [5] Random testing in Isabelle/HOL
    Berghofer, S
    Nipkow, T
    [J]. PROCEEDINGS OF THE SECOND INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, 2004, : 230 - 239
  • [6] Domain Specific Languages (DSLs) for Network Protocols (Position Paper)
    Bhatti, Saleem
    Brady, Edwin
    Hammond, Kevin
    McKinna, James
    [J]. ICDCS: 2009 INTERNATIONAL CONFERENCE ON DISTRIBUTED COMPUTING SYSTEMS WORKSHOPS, 2009, : 208 - +
  • [7] Bove A, 2009, LECT NOTES COMPUT SC, V5674, P73, DOI 10.1007/978-3-642-03359-9_6
  • [8] Brady Edwin, 2012, Practical Aspects of Declarative Languages. Proceedings 14th International Symposium, PADL 2012, P242, DOI 10.1007/978-3-642-27694-1_18
  • [9] Brady E., 2017, Type-driven Development with Idris
  • [10] Brady E, 2021, Arxiv, DOI [arXiv:2104.00480, 10.4230/LIPIcs.ECOOP.2021.9, DOI 10.4230/LIPICS.ECOOP.2021.9]
12345