데이터 추상화, 구현, 명세 및 테스트

데이터 추상화 구현 언어(SIMULA 클래스로부터 파생됨)와 대수적 공리에 의한 명세를 결합한 컴파일러 기반 시스템 DAISTS가 설명된다. 컴파일러는 공리와 구현 코드를 나타내는 두 개의 독립적인 구문 객체를 제시받고, 전자를 테스트 드라이버로 사용하여 후자로 구성된 "프로그램"을 컴파일한다. 추상 함수와 상수 값을 사용하는 표현 형태로 데이터 포인트가 이 프로그램에 공급되어 구현과 공리가 일치하는지 확인된다. 과정 중에 구조적 테스트 측정이 코드와 공리 모두에 적용되어 테스트 데이터를 평가할 수 있다. 성공적인 테스트가 공리와 코드의 일관성을 결정적으로 입증하지는 않지만, 실제로 테스트가 성공하는 경우는 드물며 오류를 드러낸다. 기존 프로그래밍 시스템에 비해 장점은 세 가지이다: