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 条

[21] CORRECTNESS PROOFS FOR ABSTRACT IMPLEMENTATIONS
BERNOT, G
INFORMATION AND COMPUTATION, 1989, 80 (02) : 121 - 151
[22] CORRECTNESS PROOFS OF CSP PROGRAMS
SOUNDARARAJAN, N
THEORETICAL COMPUTER SCIENCE, 1983, 24 (02) : 131 - 141
[23] ABSTRACT IMPLEMENTATIONS AND CORRECTNESS PROOFS
BERNOT, G
BIDOIT, M
CHOPPY, C
LECTURE NOTES IN COMPUTER SCIENCE, 1986, 210 : 236 - 251
[24] ABSTRACT IMPLEMENTATIONS AND THEIR CORRECTNESS PROOFS
NOURANI, CF
JOURNAL OF THE ACM, 1983, 30 (02) : 343 - 359
[25] Correctness proofs of distributed algorithms
Reisig, W
THEORY AND PRACTICE IN DISTRIBUTED SYSTEMS, 1995, 938 : 164 - 177
[26] Integrating Droplet into Applab - Improving The Usability of a Blocks-Based Text Editor
Bau, David Anthony
2015 IEEE BLOCKS AND BEYOND WORKSHOP (BLOCKS AND BEYOND), 2015, : 55 - 57
[27] A Usability Analysis of Blocks-based Programming Editors using Cognitive Dimensions
Holwerda, Robert
Hermans, Felienne
2018 IEEE SYMPOSIUM ON VISUAL LANGUAGES AND HUMAN-CENTRIC COMPUTING (VL/HCC), 2018, : 217 - 225
[28] Local-adaptive Blocks-based Predictor For Lossless Image Compression
Novikov, Dmitriy
Egorov, Nickolay
Gilmutdinov, Marat
2016 XV INTERNATIONAL SYMPOSIUM PROBLEMS OF REDUNDANCY IN INFORMATION AND CONTROL SYSTEMS (REDUNDANCY), 2016, : 92 - 99
[29] Smooth blocks-based blind watermarking algorithm in compressed DCT domain
Qi, Chun
Zhou, Haitao
Long, Bin
SECRYPT 2006: PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON SECURITY AND CRYPTOGRAPHY, 2006, : 347 - +
[30] A blocks-based serious game to support introductory computer programming in undergraduate education
Vahldick, Adilson
Farah, Paulo Roberto
Marcelino, Maria Jose
Mendes, Antonio Jose
COMPUTERS IN HUMAN BEHAVIOR REPORTS, 2020, 2

← 1 2 3 4 5 →