Imagen de Portada
Código QR

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

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:
SPARK (Computer program language)
Programming languages
Electronic data processing
Computer programming
Computer software development
Computer software correctness
Acceso en línea:Ver este registro en EBSCOhost
Sumario: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.