높은 무결성 시스템을위한 프로그래밍 언어 선택

Question

높은 무결성 시스템에 적합한 프로그래밍 언어는 무엇입니까?

나쁜 선택의 예는 프로그래머가 액세스 할 수없는 상당한 양의 코드가 있기 때문에 Java입니다. 프로그래머가 코드의 100 %를 담당하는 강력한 형식의 블록 구조화 된 언어의 예제를 찾고 있는데 JVM과 같은 것들로부터 가능한 한 적은 간섭이 있습니다.

컴파일러가 분명히 문제가됩니다. 언어는 완전하고 모호하지 않은 정의가 있어야합니다.

편집 : 높은 무결성 시스템은 안전 핵심 시스템 등 안전 시스템에 대한 포괄적 인 용어입니다 등

편집 편집 : 같은를 생성합니다 나는 플랫폼에 영향을받지되는 언어의 예를 원하는, 결과는 컴파일러에 관계없이 완전히 정의됩니다.

Answer 1

Ada의 SPARK 하위 집합은 매우 좋은 출발점이 될 것입니다. SPARK는 정의되지 않은 기능이 없으므로 Ada의 모든 좋은 기능 (강력한 입력, 읽기 쉬운 ...)을 상속합니다. 즉, 모든 SPARK 프로그램은 어느 Ada 컴파일러를 사용 하던지간에 똑같은 작업을 수행합니다. 그것을 컴파일하십시오.

SPARK는 런타임없이 사용할 수 있습니다. Ada 언어 (pragma No_Runtime 참조)와 유사합니다.

물론 SPARK와 같은 언어를 사용하면 안전 (또는 보안)을위한 유연성을 교환 할 수 있습니다.

Answer 2

ADA가 일반적으로 사용됩니다.

Answer 3

이것은 모순입니다. 강력하게 유형화 된 블록 구조화 언어는 컴파일러가 컴파일하여 프로그래머가 책임지지 않는 기계어 코드를 생성합니다. 코드를 100 % 책임지고 싶다면 어셈블리 언어를 사용해야합니다.

Answer 4

원하는 것을 찾을 수는 있지만 얻을 수는 없습니다.

귀하의 요구 사항은 서로 호환되지 않습니다. 그들은 기본적으로 모든 종류의 라이브러리를 배제합니다. C/C++을 사용할 수 있다고 말할 수 있습니다. 그러나 파일과 표준 라이브러리 (프로그래머가 분명히 책임지지 않음)를 사용하지 않아도됩니다.

이것은 당신을 거의 마른 땅에 남겨 둡니다. 요구 사항은 비현실적입니다. 대규모 팀이 있더라도 대부분의 라이브러리를 다시 프로그래밍하고 싶지는 않습니다.

Java는 실제로 적절한 프로그래밍 방식을 사용하면 꽤 좋습니다. 요구 사항 (높은 무결성 시스템)은 훨씬 더 프로그래밍 방법론의 문제입니다 (단위 테스트, 수많은 내부 테스트, 병렬로 구성된 여러 인스턴스). 언어가 결정하는 것보다 우주 왕복선 제어 컴퓨터 같은 결과를 비교해보십시오.

Answer 5

사전 및 사후 조건을 강화하면 무결성 시스템을보다 쉽게 ​​만드는 곳에서 Eiffel으로 생각할 수 있습니다.

Answer 6

"높은 무결성 시스템"이 무엇인지 완전히 이해하지 못합니다. "버그가 적은 시스템"을 의미한다고 가정하면 ML을 살펴보고 OOP 파생 상품 인 O'CaML을 제안합니다. ML은 유형 오류를 최소화하도록 설계되었습니다. ML에는 캐스팅 오류나 널 포인터가 없습니다. 코드를 작성할 수 없습니다.또한 역동적 인 기능이 부족하여 시원하지만 안전합니다.

그런 말로하면 ML은 해커의 즐거움에서 멀리 떨어져 있습니다. 다소 성가신 언어입니다. 그러나 한시간 더 일하고 한 가지 예외를 덜 받기를 원하면 관련 선택 사항입니다.

Answer 7

얼마나 높은 통합 성을 원하십니까? 오리건 주 포틀랜드에서

• Galois

  는 Haskell에 기록 된 고집적 시스템에서 매우 성공적인 사업을 구축했다. 데이터 무결성과 보안을 강조한다고 생각합니다. 매우 복잡한 런타임 시스템으로 이러한 복잡한 언어에서 이런 종류의 작업을 수행하는 것은 다소 놀라운 일이지만 하스켈의 유형 시스템은 매우 강력한 보장을 제공하며 언어 의미 체계는 대부분의 언어보다 훨씬 강력한 추론 원칙을 제공합니다. 또한 응용 프로그램 당 코드를 적게 작성하는 경향이 있으므로 올바른 표시가 쉽습니다.

• 더욱 강력한 보증이 필요한 경우 SPARK Ada (요즘에는 SPARK 만 사용)은 완전한 형식적 의미와 완전한 형식 확인을위한 도구와 함께 제공되는 비교적 간단하고 전통적인 명령형 언어입니다. 당신은 하스켈보다 더 강한 보증을 받지만, 자본과 노동면에서 훨씬 높은 가격으로 보장합니다.