Lựa chọn ngôn ngữ lập trình cho các hệ thống toàn vẹn cao

Question

Ngôn ngữ lập trình nào là lựa chọn tốt cho các hệ thống toàn vẹn cao?

Ví dụ về lựa chọn không đúng là Java vì có một số lượng đáng kể mã không thể truy cập được đối với lập trình viên. Tôi đang tìm kiếm các ví dụ về các ngôn ngữ có cấu trúc khối, được đánh mạnh, trong đó lập trình viên chịu trách nhiệm 100% mã và có ít sự can thiệp từ những thứ như JVM nhất có thể.

Trình biên dịch rõ ràng sẽ là một vấn đề. Ngôn ngữ phải có định nghĩa hoàn chỉnh và rõ ràng.

EDIT: cao Liêm Systems là một thuật ngữ chung cho an toàn hệ thống quan trọng vv, Hệ thống an toàn, vv

EDIT EDIT: Tôi muốn ví dụ về ngôn ngữ mà không bị ảnh hưởng bởi nền tảng, đó sẽ sản xuất cùng kết quả bất kể trình biên dịch và được định nghĩa đầy đủ.

Answer 1

Tập hợp SPARK của Ada sẽ là điểm khởi đầu rất tốt. SPARK thừa hưởng tất cả các tính năng tốt của Ada (gõ mạnh, dễ đọc, ...) với lợi ích bổ sung là không có các tính năng không xác định, nghĩa là tất cả các chương trình SPARK sẽ làm điều tương tự, bất kể trình biên dịch Ada nào đã được sử dụng biên dịch nó.

SPARK có thể được sử dụng mà không có thời gian chạy. Tương tự cho ngôn ngữ Ada (xem pragma No_Runtime).

Tất nhiên với các ngôn ngữ như SPARK bạn đang giao dịch linh hoạt cho an toàn (hoặc bảo mật).

Answer 2

Tôi nghĩ ADA thường được sử dụng cho việc này.

Answer 3

Đây là mâu thuẫn trong điều khoản. Được đánh máy mạnh mẽ, các ngôn ngữ có cấu trúc khối hầu như luôn được biên dịch bởi một trình biên dịch, tạo ra mã máy mà lập trình viên không chịu trách nhiệm. Nếu bạn muốn chịu trách nhiệm 100% mã, bạn cần sử dụng ngôn ngữ lắp ráp.

Answer 4

Bạn có thể tìm kiếm những gì bạn muốn, nhưng bạn sẽ không nhận được nó.

Yêu cầu của bạn không tương thích với nhau. Về cơ bản, họ hoàn toàn loại trừ bất kỳ loại thư viện nào. Bạn có thể nói rằng bạn có thể sử dụng C/C++ - nhưng KHÔNG CÓ BẤT K IN LOẠI BAO GỒM VÀ TIÊU CHUẨN TIÊU CHUẨN (mà lập trình viên rõ ràng sẽ không chịu trách nhiệm).

Điều này khiến bạn khá nhiều trong đất khô - yêu cầu không thực tế. Ngay cả với một nhóm lớn, một người sẽ không muốn lập trình lại hầu hết các thư viện.

Java khá tốt nếu bạn có phương pháp lập trình thích hợp - và đủ thú vị yêu cầu của bạn (hệ thống toàn vẹn cao) là một vấn đề về phương pháp lập trình (kiểm thử đơn vị, tấn kiểm thử nội bộ, nhiều trường hợp song song) so sánh kết quả - như máy tính điều khiển tàu con thoi - trong trường hợp một trục trặc) so với thứ gì đó mà ngôn ngữ quyết định.

Answer 5

Bạn có thể muốn suy nghĩ theo điều khoản của Eiffel, trong đó việc thực thi mạnh mẽ hơn trước và sau điều kiện làm cho hệ thống toàn vẹn cao dễ dàng hơn.

Answer 6

Tôi không hiểu đầy đủ về "hệ thống toàn vẹn cao". Giả sử rằng bạn có nghĩa là "một hệ thống để lại ít chỗ cho lỗi", tôi đề nghị bạn hãy xem ML, và nó là dẫn xuất OOP, O'CaML. ML được thiết kế để giảm thiểu lỗi loại. Không có lỗi đúc hoặc con trỏ null trong ML - Bạn chỉ đơn giản là không thể mã chúng.Nó cũng thiếu các tính năng động - Làm cho nó ít mát mẻ hơn nhưng an toàn hơn.

Có nói rằng, ML là xa là một niềm vui của tin tặc; Đó là một ngôn ngữ hơi cồng kềnh. Nhưng nếu bạn thích làm việc nhiều hơn một giờ và nhận được một ngoại lệ ít hơn, đó là một lựa chọn phù hợp.

Answer 7

Bạn đang tìm kiếm mức độ tích hợp cao như thế nào?

• Galois ở Portland, Oregon đã xây dựng được một doanh nghiệp rất thành công trên các hệ thống toàn vẹn cao viết bằng Haskell. Tôi tin rằng họ nhấn mạnh tính toàn vẹn và bảo mật dữ liệu. Có một điều ngạc nhiên khi làm loại công việc này bằng ngôn ngữ phức tạp, với hệ thống thời gian chạy rất phức tạp, nhưng hệ thống kiểu Haskell cung cấp sự bảo đảm rất mạnh mẽ, và ngữ nghĩa ngôn ngữ cung cấp các nguyên tắc lý luận mạnh hơn hầu hết các ngôn ngữ. Ngoài ra, bạn có xu hướng viết ít mã hơn cho mỗi ứng dụng, vì vậy nó rất dễ hiển thị chính xác.

• Nếu bạn cần đảm bảo mạnh hơn, SPARK Ada (hoặc chỉ SPARK những ngày này) là một ngôn ngữ mệnh lệnh truyền thống tương đối đơn giản đi kèm với ngữ nghĩa chính thức đầy đủ và các công cụ để xác minh chính thức đầy đủ. Bạn nhận được bảo lãnh mạnh mẽ hơn bạn sẽ với Haskell, nhưng ở một mức giá cao hơn mugh, cả về vốn và lao động.