• DocumentCode
    1648193
  • Title

    Refining logic programs using types

  • Author

    Colvin, Robert ; Hayes, Ian ; Strooper, Paul

  • Author_Institution
    Software Cerification Res. Center, Queensland Univ., Qld., Australia
  • fYear
    2000
  • fDate
    6/22/1905 12:00:00 AM
  • Firstpage
    43
  • Lastpage
    50
  • Abstract
    The logic programming refinement calculus is a method for transforming specifications to executable code, maintaining the correctness of the code with respect to its specification. In this paper we show how types can be handled in the logic programming refinement calculus. Types of variables are necessary for a complete specification of a procedure, and typing information can guide the refinement of a procedure specification to code. As an application of this framework, we show how dynamic type-checks can be formally eliminated from a sample program
  • Keywords
    formal specification; logic programming; refinement calculus; code correctness; executable code; logic programs refinement; refinement calculus; specifications; types; typing information; Calculus; Computer science; Electronic mail; Logic programming;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Computer Science Conference, 2000. ACSC 2000. 23rd Australasian
  • Conference_Location
    Canberra, ACT
  • Print_ISBN
    0-7695-0518-X
  • Type

    conf

  • DOI
    10.1109/ACSC.2000.824379
  • Filename
    824379
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=1648193