프로그램의 구조적 합성

Structural synthesis of programs

프로그램의 구조적 합성(SSP)은 명제 미적분에 기초한 특별한 형태의 (자동) 프로그램 합성입니다.보다 정확하게는, 프로그램의 구조를 서브루틴이나 심지어 컴퓨터 명령어와 같은 조각들로부터 프로그램을 자동으로 구성할 수 있도록 자세하게 설명하기 위해 직관주의적 논리를 사용합니다.이러한 조각이 올바르게 구현된 것으로 가정되므로 이 조각의 정확성을 확인할 필요가 없습니다.SSP는 서비스 지향 아키텍처를 위한 서비스 자동 구성[1] 및 대규모 시뮬레이션 프로그램 [2][3]합성에 적합합니다.

역사

자동 프로그램 합성은 인공지능 분야에서 시작되었으며, 자동 문제 해결을 위한 소프트웨어를 사용했습니다.최초의 프로그램 신시사이저는 1969년 [4]코델 그린에 의해 개발되었습니다.거의 동시에, R을 포함한 수학자들. 순경, Z. 마나, 그리고 R. Waldinger는 자동 프로그램 합성을 위한 형식 논리의 가능한 사용을 설명했습니다.실질적으로 적용 가능한 프로그램 신시사이저는 상당히 나중에 등장했습니다.

프로그램의 구조적 합성에 대한 아이디어는 1979년 Andrey Ershov와 Donald Knuth에 의해 조직된 현대 수학과 컴퓨터 과학의 알고리즘에 관한 회의에서 소개되었습니다.그 아이디어는 G에서 비롯되었습니다. 문제 [6]해결에 관한 Polya의 유명한 책.SSP에서 문제를 해결하기 위한 계획을 고안하는 방법은 공식적인 시스템으로 제시되었습니다.시스템의 추론 규칙은 G. Mints와 E에 의해 재구성되고 논리적으로 정당화되었습니다.1982년의 Tyugu.SSP를 사용하는 프로그래밍 도구 PRIZ는[8] 1980년대에 개발되었습니다.

SSP를 지원하는 최근의 통합 개발 환경은 CoCoViLa로 도메인별 언어를 구현하고 대규모 Java 프로그램을 개발하기 위한 모델 기반 소프트웨어 개발 플랫폼입니다.

SSP의 논리

프로그램의 구조적 합성은 함수로 간주될 수 있는 이미 구현된 구성 요소(예: 컴퓨터 명령 또는 소프트웨어 객체 방법)로부터 프로그램을 구성하는 방법입니다.함수의 적용 가능성에 대한 공리를 작성함으로써 직관적인 명제 논리에서 합성에 대한 사양이 제공됩니다.함수 f의 적용 가능성에 대한 공리는 논리적 의미입니다.

X1 ∧ X2 ∧ ...Xm → Y1 ∧ Y2...Yn,

여기서1 X, X2, ...는m 전제 조건이고1 Y, Y2, ...는 전제 조건입니다.Y는n 함수 f 적용의 사후 조건입니다.직관주의 논리학에서, 함수 f는 이 공식의 실현이라고 불립니다.전제 조건은 입력 데이터가 존재한다는 명제일 수 있습니다. 예를i 들어, X는 "변수i x가 값을 받았습니다"라는 의미를 가질 수 있지만, 함수 f를 사용하는 데 필요한 자원을 사용할 수 있다는 등의 다른 조건을 나타낼 수도 있습니다.전제 조건은 위에 제시된 공리와 동일한 형식의 의미일 수도 있으며, 이를 하위 작업이라고 합니다.하위 작업은 함수 f가 적용될 때 입력으로 사용할 수 있어야 하는 함수를 나타냅니다.이 기능 자체는 SSP 과정에서 합성되어야 합니다.이 경우 공리의 실현은 고차 함수, 즉 다른 함수를 입력으로 사용하는 함수입니다.예를 들어, 공식은

(상태 → nextState) ∧ 초기 상태 → 결과

두 개의 입력과 출력 결과로 고차 함수를 지정할 수 있습니다.첫 번째 입력은 상태에서 다음 상태를 계산하기 위해 합성해야 하는 함수이고, 두 번째 입력은 초기 상태입니다.고차 함수는 SSP에 일반성을 부여합니다. 합성된 프로그램에 필요한 모든 제어 구조는 사전 프로그래밍되고 각 사양에 따라 자동으로 사용될 수 있습니다.특히, 여기에 제시된 마지막 공리는 복잡한 프로그램의 사양입니다. 즉, 시스템 상태에서 nextState를 계산할 수 있는 모델에서 동적 시스템을 시뮬레이션하기 위한 시뮬레이션 엔진입니다.

레퍼런스

  1. ^ Maigre, Rina, Küngas, Peep et al.(2009).연합 정부 정보 시스템의 대규모 서비스 모델에 대한 동적 서비스 통합.지능형 시스템의 발전에 관한 국제 저널, 2(1), 181 - 191.
  2. ^ 코카스, 바후르, 오자마, 안드레스, 그리고렌코, 파벨 외 (2011).다기능 시뮬레이션 플랫폼으로서의 CoCoViLa.In: SIMUTOOLS 2011 - 제4회 시뮬레이션 도구 및 기술에 관한 국제 ICST 컨퍼런스: 3월 21-25일 - 스페인 바르셀로나: 브뤼셀: ICST, 2011, [1 - 8].
  3. ^ 그로스슈미트, 군나르; 하프, 메이트 (2009).COCO-SIM - 유체 전력 시스템을 위한 객체 지향 다극 모델링 및 시뮬레이션 환경.1부: 기본 원리.국제 유체 동력 저널, 10(2), 91 - 100.
  4. ^ Green, Cordell (1969) 문제 해결에 대한 정리 증명의 적용.인공지능에 관한 국제 공동 회의의 의사록.도널드 E.워커와 루이스 M.Norton, 편집자, Gordon and Breach Science Publishers, 뉴욕, 뉴욕, 219–239.
  5. ^ Tyugu, E.H. (1981).프로그램의 구조적 합성.인: 현대 수학 및 컴퓨터 과학의 알고리즘: 프로시저, 우르겐치, 우즈베키스탄 SSR 1979년 9월 16일-22일: 에르쇼프, A.P.; 크누스, D.E. (편집)베를린: Springer, 1981 (컴퓨터 과학 강의 노트; 122), 290 - 303.
  6. ^ Polya, G. (1957) 해결 방법프린스턴 대학 출판부
  7. ^ Mints, G.; Tyugu, E. (1982).프로그램의 구조적 합성에 대한 정당성.컴퓨터 프로그래밍 과학, 215 - 240.
  8. ^ Mints, G.; Tyugu, E. (1988).프로그래밍 시스템 PRIZ.기호 계산 저널, 5(3), 359 - 375.
  9. ^ http://www.cs.ioc.ee/cocovila

외부 링크