Thumbnail
Access Restriction
Subscribed

Author Gegg-Harrison, Timothy S.
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©2005
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Formal methods ♦ Axiomatic semantics ♦ Loop invariants ♦ Program verification ♦ Programming by contract ♦ Programming tools ♦ Weakest preconditions
Abstract Although computer scientists understand the importance of discrete mathematics to the foundations of their field, computer science (CS) students do not always see the relevance. Thus, it is important to find a way to show students its relevance. The concept of program correctness is generally taught as an activity independent of the programming process, hence many CS students perceive it as unnecessary, and even irrelevant. The concept of contracts, on the other hand, is generally taught as an integral part of the programming process. Most CS students have little difficulty understanding the need to establish contracts via preconditions and postconditions. In order to improve teaching program correctness concepts, we implemented ProVIDE, an enhanced integrated development environment (IDE). ProVIDE assists student programmers in contract construction. Rather than asking for both a precondition and postcondition for each of the student's methods, ProVIDE asks the student to simply supply a postcondition. ProVIDE then helps the student construct the appropriate precondition by leading him or her through an axiomatic proof of the method's correctness. Thus, the proof of of the method's correctness is a side-effect of the student's need to construct an appropriate precondition.
ISSN 15314278
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2005-06-01
Publisher Place New York
e-ISSN 15314278
Journal Journal on Educational Resources in Computing (JERIC)
Volume Number 5
Issue Number 2


Open content in new tab

   Open content in new tab
Source: ACM Digital Library