Co-Developing Programs and Their Proof of Correctness.

The article focuses on the auto-active approach for co-developing programs and their proof of correctness, specifically the open source SPARK technology. The authors discuss the key design and technological choices for SPARK, which made it successful within the industry, and explore the possible fut...

Descripción completa

Detalles Bibliográficos
Publicado en:Communications of the ACM Vol. 67; no. 3; pp. 84 - 95
Autores principales: Chapman, Roderick, Dross, Claire, Matthews, Stuart, Moy, Yannick
Formato: Artículo
Publicado: Association for Computing Machinery Mar2024
Materias:
Acceso en línea:Ver este registro en EBSCOhost
fields @attributes:
  recordID: 1
pdfLink:
plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=175599200&site=ehost-live
header:
  @attributes:
    shortDbName: hlh
    uiTerm: 175599200
    longDbName: Humanities International Complete
    uiTag: AN
  controlInfo:
    bkinfo:
    jinfo:
      jid:
        00010782
        ACM
      jtl: Communications of the ACM
      issn: 00010782
      maglogo: N
    pubinfo:
      dt: Mar2024
      vid: 67
      iid: 3
      pid: 68
      pub: Association for Computing Machinery
    artinfo:
      ui:
        175599200
        10.1145/3624728
      ppf: 84
      ppct: 11
      formats:
      tig:
        atl: Co-Developing Programs and Their Proof of Correctness.
      aug:
        au:
          Chapman, Roderick
          Dross, Claire
          Matthews, Stuart
          Moy, Yannick
        affil:
          Amazon Development Centre, London, U.K
          AdaCore, Île-de-France, Paris, France
          Capgemini Engineering, Bath, U.K
      su:
        SPARK (Computer program language)
        Programming languages
        Electronic data processing
        Computer programming
        Computer software development
        Computer software correctness
      sug:
        subj:
          SPARK (Computer program language)
          Programming languages
          Electronic data processing
          Computer programming
          Computer software development
          Computer software correctness
      ab: The article focuses on the auto-active approach for co-developing programs and their proof of correctness, specifically the open source SPARK technology. The authors discuss the key design and technological choices for SPARK, which made it successful within the industry, and explore the possible future of SPARK and other analyzers of the same family.
      pubtype: Periodical
      doctype: Article
      src: R
    language: English
    refInfo:
    copyright:
      @attributes:
        flag: Y
      dt:
        @attributes:
          year: 2024
    holdings:
      @attributes:
        islocal: N