Automatic Verification of Dafny Programs with Traits

被引：3
|
作者：
Ahmadi, Reza [1 ]
Leino, K. Rustan M. [2 ]
Nummenmaa, Jyrki [1 ]
机构：
[1] Univ Tampere, Tampere, Finland
[2] Microsoft Res, Redmond, WA USA
来源：
17TH WORKSHOP ON FORMAL TECHNIQUES FOR JAVA-LIKE PROGRAMS (FTFJP 2015) | 2015年
关键词：
Program Verification; Dafny; Traits; Boogie;
D O I：
10.1145/2786536.2786542
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
This paper describes the design of traits, abstract superclasses, in the verification-aware programming language Dafny. Although there is no inheritance among classes in Dafny, the traits make it possible to describe behavior common to several classes and to write code that abstracts over the particular classes involved. The design incorporates behavioral specifications for a trait's methods and functions, just like for classes in Dafny. The design has been implemented in the Dafny tool.
引用
收藏
页数：5
相关论文
共 50 条
  • [1] Exploring Automatic Specification Repair in Dafny Programs
    Abreu, Alexandre
    Macedo, Nuno
    Mendes, Alexandra
    [J]. 2023 38TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING WORKSHOPS, ASEW, 2023, : 105 - 112
  • [2] Mechanised Verification Patterns for Dafny
    Grov, Gudmund
    Lin, Yuhui
    Tumas, Vytautas
    [J]. FM 2016: FORMAL METHODS, 2016, 9995 : 326 - 343
  • [3] Accessible Software Verification with Dafny
    Leino, K. Rustan M.
    [J]. IEEE SOFTWARE, 2017, 34 (06) : 94 - 97
  • [4] Deductive Verification of Smart Contracts with Dafny
    Cassez, Franck
    Fuller, Joanne
    Quiles, Horacio Mijail Anton
    [J]. FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS (FMICS 2022), 2022, 13487 : 50 - 66
  • [5] Developing Verified Programs with Dafny
    Leino, K. Rustan M.
    [J]. VERIFIED SOFTWARE: THEORIES, TOOLS, EXPERIMENTS, 2012, 7152 : 82 - 82
  • [6] Developing Verified Programs with Dafny
    Leino, K. Rustan M.
    [J]. PROCEEDINGS OF THE 35TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE 2013), 2013, : 1488 - 1490
  • [7] AUTOMATIC VERIFICATION OF FUNCTIONAL PROGRAMS
    DROBUSHEVICH, GA
    ZUBOVICH, KA
    [J]. CYBERNETICS, 1990, 26 (04): : 491 - 502
  • [8] AN EXPERIMENT IN AUTOMATIC VERIFICATION OF PROGRAMS
    WEINBERG, GM
    GRESSETT, GL
    [J]. COMMUNICATIONS OF THE ACM, 1963, 6 (10) : 610 - 613
  • [9] Verification of Scapegoat Trees Using Dafny
    Wang, Jiapeng
    Chen, Sini
    Zhu, Huibiao
    [J]. NASA FORMAL METHODS, NFM 2024, 2024, 14627 : 118 - 135
  • [10] Deductive verification of smart contracts with Dafny
    Franck Cassez
    Joanne Fuller
    Horacio Mijail Antón Quiles
    [J]. International Journal on Software Tools for Technology Transfer, 2024, 26 : 131 - 145
12345