Title
Engineering Software Correctness
Abstract
Design and quality are fundamental themes in engineering education. Functional programming builds software from small components, a central element of good design, and facilitates reasoning about correctness, an important aspect of quality. Software engineering courses that employ functional programming provide a platform for educating students in the design of quality software. This pearl describes experiments in the use of ACL2, a purely functional subset of Common Lisp with an embedded mechanical logic, to focus on design and correctness in software engineering courses. Students find the courses challenging and interesting. A few acquire enough skill to use an automated theorem prover on the job without additional training. Many students, but not quite a majority, find enough success to suggest that additional experience would make them effective users of mechanized logic in commercial software development. Nearly all gain a new perspective on what it means for software to be correct and acquire a good understanding of functional programming.
Year
DOI
Venue
2007
10.1017/S095679680700634X
J. Funct. Program.
Keywords
Field
DocType
good design,engineering education,engineering software correctness,software engineering course,functional programming,quality software,additional training,additional experience,commercial software development,functional subset,embedded mechanical logic,computational logic,software engineering,declarative programming
Programming language,Software design,Computer science,Theoretical computer science,Software development process,Component-based software engineering,Software construction,Software quality,Software framework,Software development,Social software engineering
Journal
Volume
Issue
ISSN
17
6
0956-7968
Citations 
PageRank 
References 
5
0.48
4
Authors
1
Name
Order
Citations
PageRank
Rex Page1247.40