A Blocks-based Language for Program Correctness Proofs

被引：0
|
作者：
Osera, Peter-Michael [1 ]
Wonnacott, David G. [2 ]
机构：
[1] Grinnell Coll, Dept Comp Sci, Grinnell, IA 50112 USA
[2] Haverford Coll, Dept Comp Sci, Haverford, PA 19041 USA
来源：
2017 IEEE BLOCKS AND BEYOND WORKSHOP (B&B) | 2017年
关键词：
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
While formal mathematical reasoning is the cornerstone of computer science, undergraduates often fail to appreciate the value of mathematical proof in their studies. To alleviate this problem, we propose a novel pedagogy uniting logical reasoning with proofs of program correctness along with a proof assistant, ORC(2)A, that helps students author proofs in this domain. One of the defining features of ORC(2)A is that it has a blocks-based surface language of proof to reduce friction when adopting the tool in the classroom. We report on the current progress on ORC(2)A, in particular, its blocks-based interface, current design consideration, and our plans for evaluating the system.
引用
收藏
页码：49 / 52
页数：4
相关论文
共 50 条
  • [1] Blocks, Blocks, and More Blocks-Based Programming
    Selwyn-Smith, Ben
    Anslow, Craig
    Homer, Michael
    PROCEEDINGS OF THE 1ST ACM SIGPLAN INTERNATIONAL WORKSHOP ON PROGRAMMING ABSTRACTIONS AND INTERACTIVE NOTATIONS, TOOLS, AND ENVIRONMENTS, PAINT 2022, 2022, : 35 - 47
  • [2] Programming language elements for correctness proofs
    Department of Programming Languages and Compilers, Faculty of Informatics, Eötvös Loránd University, Budapest, Hungary
    Acta Cybern, 2008, 3 (403-425):
  • [3] Programming Language Elements for Correctness Proofs
    Devai, Gergely
    ACTA CYBERNETICA, 2008, 18 (03): : 403 - 425
  • [4] AN ABSTRACT PROGRAMMING LANGUAGE AND CORRECTNESS PROOFS
    LIU, SY
    COMPUTER LANGUAGES, 1993, 18 (04): : 273 - 282
  • [5] ON FORMAL AND INFORMAL PROOFS FOR PROGRAM CORRECTNESS
    CULIK, K
    SIGPLAN NOTICES, 1983, 18 (01): : 23 - 28
  • [6] FORMAL CORRECTNESS PROOFS OF A NONDETERMINISTIC PROGRAM
    UPFAL, E
    INFORMATION PROCESSING LETTERS, 1982, 14 (02) : 86 - 92
  • [7] PROOFS, PROGRAM CORRECTNESS, AND SOFTWARE ENGINEERING
    MERRILL, G
    SIGPLAN NOTICES, 1983, 18 (12): : 96 - 105
  • [8] Constraint-based correctness proofs for logic program transformations
    Pettorossi, Alberto
    Proietti, Maurizio
    Senni, Valerio
    FORMAL ASPECTS OF COMPUTING, 2012, 24 (4-6) : 569 - 594
  • [9] Automatic correctness proofs for logic program transformations
    Pettorossi, Alberto
    Proietti, Maurizio
    Senni, Valerio
    LOGIC PROGRAMMING, PROCEEDINGS, 2007, 4670 : 364 - +
  • [10] Encoding the program correctness proofs as programs in PCC technology
    Pirzadeh, Heidar
    Dube, Danny
    SIXTH ANNUAL CONFERENCE ON PRIVACY, SECURITY AND TRUST, PROCEEDINGS, 2008, : 121 - +
12345