정제(컴퓨팅)

정교화는 올바른 컴퓨터 프로그램을 생산하고 기존의 프로그램을 단순화하여 그들의 공식적인 검증을 가능하게 하는 다양한 접근법을 포괄하는 컴퓨터 과학의 총칭이다.

프로그램 정제

형식적인 방법에서 프로그램 정교화는 추상적(고수준) 형식 사양을 구체적(저수준) 실행 가능한 프로그램으로 검증 가능한 변환이다.^{[citation needed]}단계적 미세화는 이 과정을 단계별로 수행할 수 있도록 한다.논리적으로 정교함은 일반적으로 함축성을 수반하지만 추가적인 합병증이 있을 수 있다.

Scrum과 같이 민첩한 소프트웨어 개발 접근방식에서 제품 백로그(요건 목록)를 점진적으로 적시에 준비하는 것도 흔히 정교화라고 한다.^[1]

데이터 정제

데이터 정교화는 추상 데이터 모델(예: 세트 측면)을 구현 가능한 데이터 구조(예: 어레이)로 변환하는 데 사용된다.^{[citation needed]}운영 개선은 시스템에 대한 운영의 사양을 실행 가능한 프로그램(예: 절차)으로 변환한다.이 과정에서 사후 조건이 강화되거나 전제 조건이 약화될 수 있다.이것은 명세서에 비결정론적(일반적으로 완전히 결정론적) 구현을 감소시킨다.

예를 들어 x ∈ {1,2,3}(여기서 x는 작업 후 변수 x의 값)을 x ∈ {1,2}, 그 다음 x ∈ {1}(으)로 세분하여 x := 1로 구현할 수 있다.x := 2와 x := 3의 구현은 이 경우에 동일하게 허용될 수 있으며, 미세화를 위해 다른 경로를 사용할 수 있다.단, 이것은 실행불가, 빈 세트에서 멤버를 선택할 수 없기 때문에 x ∈ {}(허위와 동일)로 정제하지 않도록 주의해야 한다.

재화라는 용어도 가끔 사용된다(Cliff Jones coined by Cliff Jones).형식적인 정교화가 불가능할 때 긴축은 대체 기법이다.정교함의 반대는 추상화다.

정제 미적분학

정제 미적분은 프로그램 정비를 촉진하는 공식적인 시스템이다(Hoare 로직에서 영감을 받아).FermaT Transformation System은 산업적 강도의 정교화 구현이다.B-Method는 또한 요소 언어로 정제 미적분을 확장하는 공식적인 방법이다: 그것은 산업 발전에 사용되어 왔다.

정제유형

형식 이론에서 정제형은^[2]^[3]^[4] 술어를 부여받은 유형으로, 정제된 유형의 어떤 요소도 수용하는 것으로 가정된다.귀국 형식으로 사용될 때 기능이 엔드 투 엔드 원칙 postconditions로 사용되는 정제란 형식:인스턴스를 반환 자연수 자연수만 허용되는 함수의 형식보다 5f같이 쓸 수 있습니다. 더 큰 N→{n:Nn5}{\displaystyle f:\mathbb{N}\rightarrow \{n:\mathbb{N}\와 같이 전제 조건을 표현할 수 있다., $\,n>5$ 정밀유형은 따라서 행동하위태형과 관련이 있다.

참고 항목

재화(컴퓨터 과학)

참조

^ Cho, L (2009). "Adopting an Agile Culture A User Experience Team's Journey". Agile Conference: 416. doi:10.1109/AGILE.2009.76. ISBN 978-0-7695-3768-9.
^ Freeman, T.; Pfenning, F. (1991). "Refinement types for ML" (PDF). Proceedings of the ACM Conference on Programming Language Design and Implementation. pp. 268–277. doi:10.1145/113445.113468.
^ Hayashi, S. (1993). "Logic of refinement types". Proceedings of the Workshop on Types for Proofs and Programs. pp. 157–172. CiteSeerX 10.1.1.38.6346. doi:10.1007/3-540-58085-9_74.
^ Denney, E. (1998). "Refinement types for specification". Proceedings of the IFIP International Conference on Programming Concepts and Methods. Vol. 125. Chapman & Hall. pp. 148–166. CiteSeerX 10.1.1.22.4988.

이 소프트웨어 공학 관련 기사는 단조롭다.위키피디아를 확장하여 도울 수 있다.

[1] Cho, L (2009). "Adopting an Agile Culture A User Experience Team's Journey". Agile Conference: 416. doi:10.1109/AGILE.2009.76. ISBN 978-0-7695-3768-9.

[2] Freeman, T.; Pfenning, F. (1991). "Refinement types for ML" (PDF). Proceedings of the ACM Conference on Programming Language Design and Implementation. pp. 268–277. doi:10.1145/113445.113468.

[3] Hayashi, S. (1993). "Logic of refinement types". Proceedings of the Workshop on Types for Proofs and Programs. pp. 157–172. CiteSeerX 10.1.1.38.6346. doi:10.1007/3-540-58085-9_74.

[4] Denney, E. (1998). "Refinement types for specification". Proceedings of the IFIP International Conference on Programming Concepts and Methods. Vol. 125. Chapman & Hall. pp. 148–166. CiteSeerX 10.1.1.22.4988.

[1]

[2]

[3]

[4]

Search