Lập trình giảng dạy và các phương pháp chính thức

Question

Đây là một câu hỏi kỳ lạ. Tôi đang trong quá trình viết một cuốn sách về việc học lập trình bằng cách sử dụng các phương pháp chính thức, và tôi sẽ nhắm nó vào những người có kinh nghiệm lập trình. Ý tưởng là dạy họ trở thành những lập trình viên chất lượng cao.

Ký pháp cơ bản sẽ xuất phát từ số Discipline of Programming của Dijkstra, cùng với một số tiện ích mở rộng đồng thời và liên lạc.

Không giống như EWD, tôi muốn học sinh của mình cuối cùng viết các chương trình thực thi thực tế. Điều đó có nghĩa là tại một số điểm dịch từ ký hiệu EWD sang một số ngôn ngữ khác. Khi tôi bắt đầu thực hiện lập trình chính thức, tôi nhắm mục tiêu C, nhưng cuối cùng bạn viết rất nhiều hệ thống ống nước, cộng với tất cả các phức tạp của việc xử lý con trỏ, vv. Ruby là một mục tiêu rõ ràng, như Scheme hoặc Lisp. Nhưng cũng có các ngôn ngữ chức năng khác nhau; vì tôi đặc biệt quan tâm đến đồng thời, Erlang có vẻ như là một khả năng.

Vì vậy, cuối cùng, đây là câu hỏi của tôi: Tôi nên dạy những ngôn ngữ nào để người đọc nhắm mục tiêu các chương trình phát triển chính thức của họ?

Answer 1

Charlie,

Tôi đã luôn gắn liền kiệt Dijkstra với một mô hình lập trình, trong đó giai đoạn trung tâm là chiếm đóng bởi các vòng lặp và mảng. Nếu bạn gắn bó với Dijkstra (ví dụ: tính toán các điều kiện tiên quyết yếu nhất), tôi nghĩ bạn sẽ thấy các ngôn ngữ chức năng không phù hợp lắm. Trong số các ngôn ngữ phổ biến cung cấp hỗ trợ tốt cho lập trình bắt buộc bằng các vòng lặp và mảng, có lẽ Python mang hành lý bổ sung ít nhất.

Điều này không có nghĩa là các ngôn ngữ chức năng không phù hợp với các phương thức chính thức --- chúng rất phù hợp --- nhưng phong cách khá khác với Dijkstra. Các phương pháp ưa thích nhấn mạnh các bằng chứng tính toán; xem bài báo của Richard Bird về việc giải Sudoku (nặng nề) hoặc sách giáo khoa của Richard Bird và Phil Wadler.

Đối với sự tương tranh, nó phụ thuộc rất nhiều vào mô hình đồng thời (và những phương pháp chính thức) mà bạn tin tưởng. Concurrent ML của John Reppy là một mô hình thông điệp đẹp. Erlang cũng có một mô hình hạn chế sạch đẹp. Mặt khác, lập trình với ổ khóa và các phần quan trọng là rất khó khăn, có thể có nhiều lợi ích hơn cho các phương pháp chính thức trong tình huống đó.

Hai bài phát biểu truyền khác mà bạn có thể quan tâm đến nghiên cứu nền của bạn:

• Lập trình viên duy nhất mà tôi từng gặp người áp dụng phương pháp Dijkstra trong thực tế để hệ thống thực sự là Greg Nelson, người đang làm việc tại Modula- 3. (Greg và Mark Manasse đã viết hệ thống cửa sổ Trestle với nhau.) Modula-3 là một ngôn ngữ rất hay mà Digital cho phép chết thông qua sự thiếu thận trọng và bất lực. Greg đã có một bài báo TOPLAS tốt đẹp trên một phần mở rộng để tính toán của Dijkstra.

• Ngôn ngữ lập trình của Gerard Holzmann SPIN được dựa trực tiếp vào ngôn ngữ lệnh bảo vệ của Dijkstra và cũng hỗ trợ đồng thời. Mục đích của nó là kiểm tra mô hình, không lập trình, và có một vài đồng bộ hóa, nhưng có một kết nối mạnh mẽ với các phương thức chính thức, và nó thực sự tuyệt vời để có thể mô hình kiểm tra các xác nhận của bạn. Bất cứ ai quan tâm đến các phương pháp chính thức sẽ muốn kiểm tra nó.

(Edit:. Dưới đây là một liên kết đến giấy Greg Nelson, hoặc một trong số họ - CRM)

Answer 2

Đó là một ý tưởng hay. Tôi nghĩ rằng Đề án là một lựa chọn tốt vì nó cho phép người ta đưa vào thực hành (dưới hình thức thư viện) các trừu tượng khác nhau với các yếu tố cần thiết tối thiểu. Nó cũng dễ dàng để dịch từ chương trình đến một hệ thống xác minh như PVS (http://pvs.csl.sri.com/)

cổ vũ

Answer 3

Tôi lớn lên trên Lisp và Đề án và yêu cả hai. Tôi nghĩ rằng họ là những ngôn ngữ tuyệt vời để học hỏi từ đầu. Nhưng, tôi không chắc ai đó với một số kinh nghiệm lập trình sẽ đưa đến những ngôn ngữ đó. Bạn sẽ không nhận được nhiều lượt truy cập trên Amazon cho cuốn sách của mình với Đề án trong tiêu đề. :)

C# là một ngôn ngữ rất dễ học và nó có tất cả các khái niệm cơ bản bạn sẽ cần phải đi sâu vào các chủ đề như đồng thời khá nhanh. Nó có nhiều khả năng ứng dụng hơn vì bạn cũng có thể nhắm mục tiêu đến các khái niệm OO và web. Nó cũng khá phổ biến và bạn sẽ nhận được các công ty trả tiền cho sổ nhân viên của họ mà luôn luôn là tốt cho bán hàng ("Hãy là một Kick Ass C# Programmer" đi nhiều hơn nữa trên một tấm bồi hoàn chi phí hơn "Concurrency trong Lisp hiện đại").

F # là một ngôn ngữ thú vị. Nó có vẻ đẹp chức năng của một Lisp hoặc Scheme (cũng không hoàn toàn, nhưng gần như) và nó mang lại cho bạn một số khả năng đi sâu vào các chủ đề OOP cũng như móc vào .NET Framework cho giao diện người dùng nếu bạn muốn thêm gia vị. Nhưng, ngay bây giờ, nó tối nghĩa.

Tôi không thể nói chuyện với Ruby, cá nhân, tôi sẽ cắn viên đạn và đi với C#.

Answer 4

Tôi nghĩ rằng bạn nên tự mình có một số kinh nghiệm bằng ngôn ngữ bạn sử dụng cho sách của mình hoặc ai đó thành thạo để xem lại mã của bạn.

Cá nhân, tôi muốn sử dụng Common Lisp, vì tôi quen thuộc với điều đó, và đó là một ngôn ngữ tuyệt vời để thực hiện bất kỳ khái niệm nào. Các tùy chọn khác có thể là Erlang, Haskell, Ruby hoặc Python, có lẽ ngay cả một số phương ngữ ML. Tôi thiên vị chống lại gia đình C (bao gồm cả C# và Java), họ dường như bị mắc kẹt với một mức độ suy nghĩ thấp hơn về các khái niệm.

Answer 5

Bỏ qua rõ ràng những gì favoriteprogramminglanguage bạn câu trả lời, tôi có thể thấy hai câu trả lời hữu ích:

Một mặt, bạn đang cố gắng để chứng minh phương pháp với những gì được coi là lập trình viên trung gian.Nếu bạn chọn một ngôn ngữ duy nhất và chúc lành cho nó như là ngôn ngữ sách của bạn, bạn sẽ có thể xa lánh những người đọc tiềm năng không thích ngôn ngữ đó vì một lý do nào đó. Vì bạn đang trình diễn các phương pháp, Bạn có sự sang trọng trong việc sử dụng các đoạn mã bằng các ngôn ngữ xảy ra để minh họa cho quan điểm của bạn một cách súc tích. Ví dụ: ngôn ngữ duy nhất có sẵn để trình diễn RIIA có thể là C++, nhưng ngôn ngữ này cũng khá kém để hiển thị cách thực hiện phân tích nguồn. Sơ đồ lý tưởng cho phân tích nguồn, nhưng không cung cấp cho bạn nhiều tùy chọn để khám phá các lợi ích (và điểm yếu) của việc gõ mạnh. Sử dụng nhiều ngôn ngữ.

Mặt khác, vì bạn chủ yếu là lên đến các phương pháp lập trình, tôi không hoàn toàn chắc chắn bạn cần bất kỳ ngôn ngữ thực sự nào cả. Một ký hiệu được xác định rõ ràng là tốt và buộc người đọc của bạn tập trung vào điểm bạn đang tạo ra thay vì các chi tiết bề ngoài của một ngôn ngữ này hay ngôn ngữ khác.

Answer 6

Thành thực mà nói, tôi không thể khuyên của Ruby cho việc này. Khi tôi lập trình hàng ngày trong thế giới thương mại của mình, tôi thích nó khá nhiều, chắc chắn nhiều hơn C hoặc Java.Nhưng ngữ nghĩa của nó quá yếu đến mức tôi không tin nó bằng một nửa so với C, mặc dù tôi có thể dành vài giờ tranh luận về một tuyên bố và tư vấn rằng cuốn sách trắng dày hơn nhiều thay thế K & R, tôi đi ra cuối cùng khá thuyết phục rằng nếu tôi có một trình biên dịch phù hợp (vâng, tôi biết, tôi là một người mơ mộng, nhưng làm việc với tôi ở đây) Tôi biết những gì đang xảy ra ở phía bên kia.

Ruby là tuyệt vời theo nhiều cách, nhưng theo như bất cứ điều gì chính thức đi, các twain sẽ không bao giờ đáp ứng.

Tôi muốn tự mình bỏ phiếu cho Haskell, bởi vì mỗi khi tôi quay lại, tôi đều ngạc nhiên trước ý nghĩa của mọi thứ trong định nghĩa ngôn ngữ đó. (Mặc dù phải thừa nhận chỉ sau một năm hoặc lâu hơn, tôi chắc chắn rằng tôi đã không khám phá một nửa góc của cả Haskell 98.)

Và tôi cũng hiểu rằng, Dikjstra so với chức năng; quay lại và reading his papers anh ấy rất nhiều trong thế giới bắt buộc; Tôi không đủ điều kiện để nói liệu anh ta có thực sự đi sai đường không. Có lẽ tôi chỉ bị choáng ngợp bởi cách viết của anh ấy tốt như thế nào, nhiều như suy nghĩ của anh ấy. Nhưng nó dường như làm hài lòng anh ta, vì vậy những gì về việc sử dụng Algol 60?

Answer 7

Có một số trường đại học sử dụng Perfect Developer để dạy các phương pháp chính thức (từ chối trách nhiệm: Tôi được kết nối với sản phẩm này). Nó được xây dựng xung quanh một ngôn ngữ để thể hiện thông số kỹ thuật, sàng lọc dữ liệu và thuật toán. Nó có một prover định lý tự động để xác minh, và một bộ tạo mã có thể tạo ra C++, C# và Java. Thiết kế của PD được lấy cảm hứng từ "Kỷ luật lập trình", tuy nhiên chúng tôi nhận thấy ký hiệu khá không thực tế đối với các hệ thống lớn, vì vậy ký pháp đã phân tách một phần từ Dijktra.