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 条

[41] Blocks-based Programming Languages: Simplifying Programming for Different Audiences with Different Goals
Medlock-Walton, Paul
Harms, Kyle J.
Kraemer, Eileen T.
Brennan, Karen
Wendel, Daniel
PROCEEDINGS OF THE 45TH ACM TECHNICAL SYMPOSIUM ON COMPUTER SCIENCE EDUCATION (SIGCSE'14), 2014, : 545 - 546
[42] Extending the Design of a Blocks-Based Python']Python Environment to Support Complex Types
Poole, Matthew
2017 IEEE BLOCKS AND BEYOND WORKSHOP (B&B), 2017, : 1 - 7
[43] Shared Blocks-Based Ensemble Deep Learning for Shallow Landslide Susceptibility Mapping
Kavzoglu, Taskin
Teke, Alihan
Yilmaz, Elif Ozlem
REMOTE SENSING, 2021, 13 (23)
[44] Adaptive Blocks-Based Target Tracking Method Fusing Color Histogram and SURF Features
Cao, Ruilin
Li, Qing
Zhang, Weicun
Pei, Zhao
Liu, Yichang
PROCEEDINGS OF 2016 CHINESE INTELLIGENT SYSTEMS CONFERENCE, VOL II, 2016, 405 : 193 - 200
[45] Proofs of Correctness and Properties of Integer Adder Circuits
Chen, Gang
Liu, Feng
IEEE TRANSACTIONS ON COMPUTERS, 2010, 59 (01) : 134 - 136
[46] PROOFS OF PARTIAL CORRECTNESS FOR ITERATIVE AND RECURSIVE COMPUTATIONS
COURCELLE, B
JOURNAL OF SYMBOLIC LOGIC, 1987, 52 (01) : 297 - 298
[47] CORRECTNESS OF SHORT PROOFS IN THEORY WITH NOTIONS OF FEASIBILITY
OREVKOV, VP
LECTURE NOTES IN COMPUTER SCIENCE, 1990, 417 : 242 - 245
[48] TOrPEDO: witnessing model correctness with topological proofs
Menghi, Claudio
Rizzi, Alessandro Maria
Bernasconi, Anna
Spoletini, Paola
FORMAL ASPECTS OF COMPUTING, 2021, 33 (06) : 1039 - 1066
[49] Shorter Lattice-Based Zero-Knowledge Proofs for the Correctness of a Shuffle
Herranz, Javier
Martinez, Ramiro
Sanchez, Manuel
FINANCIAL CRYPTOGRAPHY AND DATA SECURITY, FC 2021, 2021, 12676 : 315 - 329
[50] Using Upper-Elementary Student Performance to Understand Conceptual Sequencing in a Blocks-based Curriculum
Franklin, Diana
Skifstad, Gabriela
Rolock, Reiny
Mehrotra, Isha
Ding, Valerie
Hansen, Alexandria
Weintrop, David
Harlow, Danielle
PROCEEDINGS OF THE 2017 ACM SIGCSE TECHNICAL SYMPOSIUM ON COMPUTER SCIENCE EDUCATION (SIGCSE'17), 2017, : 231 - 236

← 1 2 3 4 5 →