Software refinement with Perfect Developer

Author

Carter, Gareth ; Monahan, Rosemary ; Morris, Joseph M.

Author_Institution

Dept. of Comput. Sci., Nat. Univ. of Ireland, Maynooth, Ireland

fYear

2005

fDate

7-9 Sept. 2005

Firstpage

363

Lastpage

372

Abstract

Perfect Developer is a software tool that supports the formal development of object-oriented programs by refinement, including formal verification of code. It is built around a single language that supports both specification and implementation. We critically examine how Perfect Developer supports programming by refinement, focusing on three refinement techniques: algorithm refinement, data refinement and delta refinement. In particular we examine the extent to which Perfect Developer provides formal verification for these techniques. We assess it as a tool for software construction and compare it with related tools.

Keywords

formal specification; formal verification; object-oriented programming; refinement calculus; software tools; Perfect Developer; algorithm refinement; data refinement; delta refinement; formal development; formal implementation; formal specification; formal verification; object-oriented program; software refinement; software tool; Computer applications; Computer languages; Computer science; Formal specifications; Formal verification; Partial discharges; Programming profession; Software engineering; Software tools; Testing;

fLanguage

English

Publisher

ieee

Conference_Titel

Software Engineering and Formal Methods, 2005. SEFM 2005. Third IEEE International Conference on

Print_ISBN

0-7695-2435-4

Type

conf

DOI

10.1109/SEFM.2005.41

Filename

1575926