• DocumentCode
    1401091
  • Title

    A weakest precondition semantics for refinement of object-oriented programs

  • Author

    Cavalcanti, Ana ; Naumann, David A.

  • Author_Institution
    Centro de Inf., Univ. Fed. de Pernambuco, Recife, Brazil
  • Volume
    26
  • Issue
    8
  • fYear
    2000
  • fDate
    8/1/2000 12:00:00 AM
  • Firstpage
    713
  • Lastpage
    728
  • Abstract
    We define a predicate-transformer semantics for an object oriented language that includes specification constructs from refinement calculi. The language includes recursive classes, visibility control, dynamic binding, and recursive methods. Using the semantics, we formulate notions of refinement. Such results are a first step toward a refinement calculus
  • Keywords
    formal specification; object-oriented languages; object-oriented programming; programming language semantics; refinement calculus; type theory; dynamic binding; object oriented language; object oriented program refinement; predicate-transformer semantics; recursive classes; recursive methods; refinement calculi; specification constructs; visibility control; weakest precondition semantics; Calculus; Computer Society; Formal specifications; Java; Logic programming; Object oriented modeling; Object oriented programming; Software algorithms; Terminology; Testing;
  • fLanguage
    English
  • Journal_Title
    Software Engineering, IEEE Transactions on
  • Publisher
    ieee
  • ISSN
    0098-5589
  • Type

    jour

  • DOI
    10.1109/32.879810
  • Filename
    879810
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=1401091