We devise imperative programming languages for verified real number computation where real numbers are provided as abstract data types such that the users of the languages can express real number computation by considering real numbers as abstract mathematical entities. Unlike other common approaches toward real number computation, based on an algebraic model that lacks implementability or transcendental computation, or finite-precision approximation such as using double precision computation that lacks a formal foundation, our languages are devised based on computable analysis, a foundation of rigorous computation over continuous data. Consequently, the users of the language can easily program real number computation and reason about the behaviours of their programs, relying on their mathematical knowledge of real numbers without worrying about artificial roundoff errors. As the languages are imperative, we adopt precondition-postcondition-style program specification and Hoare-style program verification methodologies. Consequently, the users of the language can easily program a computation over real numbers, specify the expected behaviour of the program, including termination, and prove the correctness of the specification. Furthermore, we suggest extending the languages with other interesting continuous data, such as matrices, continuous real functions, et cetera.
이 논문에서는 실수를 추상형 자료형으로 제공하는 명령형 프로그래밍 언어들을 고안한다. 실수라는 연속적인 자료를 추상적으로 다루는 기존의 방식으로는 크게 대수적 계산 모형에 기반하는 것과 실수를 double 등의 유한 표기법을 사용하여 근사하는 것이 있다. 대수적 계산 모형의 경우 실제로 컴퓨터에 구현할 수 없거나 초월수 등을 다룰 수 없다는 한계가 있으며 유한 표기법에 기반한 계산의 경우 엄밀한 계산 모형이 없거나 계산 결과를 신뢰할 수 없다는 문제가 존재한다. 이 논문에서는 연속형 자료에 대한 계산의 엄밀한 이론적 토대인 계산 해석학에 기반하여 위의 문제들을 해결한다. 이 논문에서 제안되는 언어들은 명령형 프로그래밍 언어로 선행 조건과 후행 조건을 통해 프로그램들을 명세할 수 있다. 또한, 이 논문에서는 명세된 프로그램들을 검증할 수 있는 호아르 방식의 프로그래밍 검증법을 정의한다. 결과적으로 사용자들은 쉽게 실수 계산을 프로그램으로 표현할 수 있으며, 작성된 프로그램의 작동 방식을 명세할 수 있고, 명세된 프로그램을 검증할 수 있다. 프로그래밍 언어들을 고안하는 단계를 프레임워크로 만들어서 행렬, 연속함수 등 다른 연속적 추상형 자료형으로 확장하는 방법 또한 제안한다.
