Đây là bài viết dịch . Nhưng trước đó có một phần giới thiệu ngắn. Zombie được hình thành như thế nào? Mọi người đều rơi vào tình huống muốn nâng tầm bạn bè hoặc đồng nghiệp lên ngang tầm với mình nhưng điều đó không thành công. Hơn nữa, “không thành công” không phải đối với bạn mà đối với anh ấy: một mặt là mức lương, nhiệm vụ bình thường, v.v., mặt khác là cần phải suy nghĩ. Suy nghĩ thật khó chịu và đau đớn. Anh ấy nhanh chóng bỏ cuộc và tiếp tục viết mã mà không cần sử dụng đến bộ não của mình. Bạn nhận ra rằng cần bao nhiêu nỗ lực để vượt qua rào cản của sự bất lực đã học được và bạn chỉ đơn giản là không làm điều đó. Đây là cách zombie được hình thành, tưởng chừng như có thể chữa khỏi nhưng có vẻ như sẽ không có ai làm điều này.
Khi tôi nhìn thấy điều đó (vâng, chính người bạn đó trong sách giáo khoa) và không phải là báo cáo mà là phiên hỏi đáp, tôi hơi cảnh giác. Để đề phòng, Leslie là một nhà khoa học nổi tiếng thế giới, là tác giả của các công trình nổi tiếng về điện toán phân tán và bạn cũng có thể biết đến anh ấy qua các chữ cái La trong LaTeX - “Lamport TeX”. Yếu tố đáng báo động thứ hai là yêu cầu của anh ta: mọi người đến đều phải (hoàn toàn miễn phí) nghe trước một số báo cáo của anh ta, đặt ra ít nhất một câu hỏi về chúng và chỉ sau đó mới đến. Tôi quyết định xem Lamport đang phát sóng gì ở đó - và nó thật tuyệt! Đây chính xác là thứ đó, một viên thuốc liên kết thần kỳ để chữa trị cho thây ma. Tôi cảnh báo bạn: văn bản có thể gây tổn hại nghiêm trọng cho những ai yêu thích các phương pháp siêu linh hoạt và những người không muốn kiểm tra những gì họ đã viết.
Sau habrokat, quá trình dịch thuật của buổi hội thảo thực sự bắt đầu. Thích đọc sách!
Dù đảm nhận nhiệm vụ nào, bạn luôn cần phải trải qua ba bước:
- quyết định mục tiêu bạn muốn đạt được;
- quyết định chính xác bạn sẽ đạt được mục tiêu của mình như thế nào;
- đạt được mục tiêu của bạn.
Điều này cũng áp dụng cho lập trình. Khi viết mã, chúng ta cần:
- quyết định chính xác chương trình nên làm gì;
- xác định chính xác nó sẽ thực hiện nhiệm vụ của mình như thế nào;
- viết mã thích hợp.
Tất nhiên, bước cuối cùng rất quan trọng nhưng tôi sẽ không nói về nó hôm nay. Thay vào đó, chúng ta sẽ thảo luận về hai điều đầu tiên. Mọi lập trình viên đều thực hiện chúng trước khi bắt đầu làm việc. Bạn không ngồi viết trừ khi bạn quyết định mình sẽ viết gì: trình duyệt hoặc cơ sở dữ liệu. Phải có một ý tưởng nhất định về mục tiêu. Và bạn chắc chắn nghĩ về chính xác những gì chương trình sẽ làm, và đừng viết nó một cách bừa bãi với hy vọng rằng bản thân mã bằng cách nào đó sẽ biến thành một trình duyệt.
Chính xác thì việc suy nghĩ trước về mã này xảy ra như thế nào? Chúng ta nên nỗ lực bao nhiêu vào việc này? Tất cả phụ thuộc vào mức độ phức tạp của vấn đề chúng ta đang giải quyết. Giả sử chúng ta muốn viết một hệ thống phân tán có khả năng chịu lỗi. Trong trường hợp này, chúng ta nên suy nghĩ kỹ mọi việc trước khi ngồi viết mã. Điều gì sẽ xảy ra nếu chúng ta chỉ cần tăng một biến số nguyên lên 1? Thoạt nhìn, mọi thứ ở đây đều tầm thường và không cần phải suy nghĩ, nhưng sau đó chúng ta nhớ rằng có thể xảy ra tình trạng tràn. Vì vậy, ngay cả để hiểu một vấn đề đơn giản hay phức tạp, trước tiên bạn cần phải suy nghĩ.
Nếu bạn suy nghĩ trước về các giải pháp khả thi cho một vấn đề, bạn có thể tránh được sai lầm. Nhưng điều này đòi hỏi suy nghĩ của bạn phải rõ ràng. Để đạt được điều này, bạn cần phải viết ra suy nghĩ của mình. Tôi thích câu nói của Dick Guindon: “Khi bạn viết, tự nhiên sẽ cho bạn thấy suy nghĩ của bạn cẩu thả đến mức nào”. Nếu bạn không viết, bạn chỉ nghĩ rằng bạn đang suy nghĩ. Và bạn cần viết ra những suy nghĩ của mình dưới dạng thông số kỹ thuật.
Thông số kỹ thuật phục vụ nhiều chức năng, đặc biệt là trong các dự án lớn. Nhưng tôi sẽ chỉ nói về một trong số đó: chúng giúp chúng ta suy nghĩ rõ ràng. Suy nghĩ rõ ràng là rất quan trọng và khá khó khăn, vì vậy chúng tôi cần bất kỳ sự trợ giúp nào ở đây. Chúng ta nên viết thông số kỹ thuật bằng ngôn ngữ nào? Nhìn chung, đây luôn là câu hỏi đầu tiên của các lập trình viên: chúng ta sẽ viết bằng ngôn ngữ nào? Không có câu trả lời đúng duy nhất: các vấn đề chúng ta giải quyết quá đa dạng. Đối với một số người, TLA+ rất hữu ích - đó là ngôn ngữ đặc tả mà tôi đã phát triển. Đối với những người khác, sử dụng tiếng Trung sẽ thuận tiện hơn. Tất cả phụ thuộc vào tình hình.
Câu hỏi quan trọng hơn là: làm thế nào chúng ta có thể có được tư duy rõ ràng hơn? Trả lời: Chúng ta phải suy nghĩ như các nhà khoa học. Đây là cách suy nghĩ đã có hiệu quả trong suốt 500 năm qua. Trong khoa học, chúng ta xây dựng các mô hình toán học về thực tế. Thiên văn học có lẽ là môn khoa học đầu tiên theo đúng nghĩa của từ này. Trong mô hình toán học được sử dụng trong thiên văn học, các thiên thể xuất hiện dưới dạng các điểm có khối lượng, vị trí và động lượng, mặc dù trên thực tế chúng là những vật thể cực kỳ phức tạp với núi non và đại dương, lên xuống và dòng chảy. Mô hình này, giống như bất kỳ mô hình nào khác, được tạo ra để giải quyết một số vấn đề nhất định. Thật tuyệt vời khi xác định nơi đặt kính thiên văn nếu bạn muốn tìm một hành tinh. Nhưng nếu bạn muốn dự đoán thời tiết trên hành tinh này, mô hình này sẽ không hoạt động.
Toán học cho phép chúng ta xác định các thuộc tính của một mô hình. Và khoa học cho thấy những tính chất này liên quan đến thực tế như thế nào. Hãy nói về khoa học của chúng ta, khoa học máy tính. Thực tế mà chúng tôi làm việc là các hệ thống máy tính thuộc nhiều loại khác nhau: bộ xử lý, bảng điều khiển trò chơi, máy tính chạy chương trình, v.v. Tôi sẽ nói về việc thực thi một chương trình trên máy tính, nhưng nhìn chung, tất cả những kết luận này đều áp dụng cho bất kỳ hệ thống máy tính nào. Trong khoa học của chúng tôi, chúng tôi sử dụng nhiều mô hình khác nhau: máy Turing, các tập hợp sự kiện được sắp xếp một phần và nhiều mô hình khác.
Chương trình là gì? Đây là bất kỳ mã nào có thể được xem xét riêng. Giả sử chúng ta cần viết một trình duyệt. Chúng tôi thực hiện ba nhiệm vụ: thiết kế bản trình bày chương trình của người dùng, sau đó viết sơ đồ cấp cao của chương trình và cuối cùng là viết mã. Khi viết mã, chúng tôi nhận ra rằng mình cần viết một trình định dạng văn bản. Ở đây một lần nữa chúng ta cần giải quyết ba vấn đề: xác định văn bản nào công cụ này sẽ trả về; chọn thuật toán định dạng; viết mã. Nhiệm vụ này có nhiệm vụ phụ riêng: chèn dấu gạch nối vào từ một cách chính xác. Chúng tôi cũng giải quyết nhiệm vụ con này theo ba bước - như chúng tôi thấy, chúng được lặp lại ở nhiều cấp độ.
Chúng ta hãy xem xét kỹ hơn bước đầu tiên: chương trình giải quyết được vấn đề gì. Ở đây chúng ta thường mô hình hóa một chương trình như một hàm nhận một số đầu vào và đưa ra một số đầu ra. Trong toán học, một hàm số thường được mô tả như một tập hợp các cặp có thứ tự. Ví dụ: hàm bình phương cho số tự nhiên được mô tả dưới dạng tập {<0,0>, <1,1>, <2,4>, <3,9>, …}. Miền định nghĩa của hàm như vậy là tập hợp các phần tử đầu tiên của mỗi cặp, tức là các số tự nhiên. Để xác định một hàm, chúng ta cần chỉ định miền và công thức của nó.
Nhưng hàm trong toán học không giống hàm trong ngôn ngữ lập trình. Toán học đơn giản hơn nhiều. Vì tôi không có thời gian cho các ví dụ phức tạp nên hãy xem xét một ví dụ đơn giản: một hàm trong C hoặc một phương thức tĩnh trong Java trả về ước số chung lớn nhất của hai số nguyên. Trong đặc tả của phương pháp này, chúng tôi sẽ viết: tính toán GCD(M,N) cho các lập luận M и NĐâu GCD(M,N) - một hàm có miền xác định là một tập hợp các cặp số nguyên và giá trị trả về là số nguyên lớn nhất được chia cho M и N. Thực tế so sánh với mô hình này như thế nào? Mô hình hoạt động với các số nguyên và trong C hoặc Java chúng ta có 32-bit int. Mô hình này cho phép chúng ta quyết định liệu thuật toán có đúng hay không GCD, nhưng nó sẽ không ngăn được lỗi tràn. Điều này đòi hỏi một mô hình phức tạp hơn và không có thời gian.
Hãy nói về những hạn chế của chức năng như một mô hình. Một số chương trình (chẳng hạn như hệ điều hành) không chỉ trả về một giá trị cụ thể cho một số đối số nhất định mà chúng có thể chạy liên tục. Ngoài ra, chức năng như một mô hình không phù hợp cho bước thứ hai: lập kế hoạch giải quyết vấn đề. Quicksort và Bubble Sort tính toán cùng một hàm nhưng chúng là các thuật toán hoàn toàn khác nhau. Vì vậy, để mô tả cách thức đạt được mục tiêu của chương trình, tôi sử dụng một mô hình khác, tạm gọi là mô hình hành vi chuẩn. Chương trình được thể hiện trong đó dưới dạng một tập hợp tất cả các hành vi hợp lệ, mỗi hành vi đó lần lượt là một chuỗi các trạng thái và trạng thái là việc gán giá trị cho các biến.
Hãy xem bước thứ hai của thuật toán Euclide sẽ như thế nào. Chúng ta cần tính toán GCD(M, N). Chúng tôi khởi tạo M như xVà N như y, sau đó liên tục trừ biến nhỏ hơn trong số các biến này khỏi biến lớn hơn cho đến khi chúng bằng nhau. Ví dụ, nếu M = 12Và N = 18, chúng ta có thể mô tả hành vi sau:
[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]
Và nếu M = 0 и N = 0? Số XNUMX chia hết cho mọi số nên không có ước số lớn nhất trong trường hợp này. Trong tình huống này, chúng ta cần quay lại bước đầu tiên và hỏi: chúng ta có thực sự cần tính GCD cho các số không dương không? Nếu điều này là không cần thiết thì bạn chỉ cần thay đổi thông số kỹ thuật.
Ở đây cần có một sự lạc đề ngắn gọn về năng suất. Nó thường được đo bằng số dòng mã được viết mỗi ngày. Nhưng công việc của bạn sẽ hữu ích hơn nhiều nếu bạn loại bỏ được một số dòng nhất định, vì bạn sẽ có ít chỗ hơn cho lỗi. Và cách dễ nhất để loại bỏ mã là ở bước đầu tiên. Có thể đơn giản là bạn không cần tất cả những thứ chuông và còi mà bạn đang cố gắng thực hiện. Cách nhanh nhất để đơn giản hóa chương trình và tiết kiệm thời gian là không làm những việc không nên làm. Bước thứ hai có khả năng tiết kiệm thời gian cao thứ hai. Nếu bạn đo lường năng suất bằng những dòng chữ viết ra thì việc nghĩ đến cách hoàn thành một nhiệm vụ sẽ khiến bạn kém năng suất, vì bạn có thể giải quyết vấn đề tương tự với ít mã hơn. Tôi không thể đưa ra số liệu thống kê chính xác ở đây, vì tôi không có cách nào để đếm số dòng mà tôi không viết do thời gian tôi dành cho đặc tả, tức là ở bước đầu tiên và bước thứ hai. Và chúng ta cũng không thể làm thí nghiệm ở đây, vì trong thí nghiệm chúng ta không có quyền hoàn thành bước đầu tiên, nhiệm vụ đã được xác định trước.
Rất dễ bỏ qua nhiều khó khăn trong các thông số kỹ thuật không chính thức. Không có gì khó khăn khi viết các thông số kỹ thuật nghiêm ngặt cho các hàm; tôi sẽ không thảo luận về vấn đề này. Thay vào đó, chúng ta sẽ nói về việc viết các thông số kỹ thuật mạnh mẽ cho các hành vi tiêu chuẩn. Có một định lý phát biểu rằng bất kỳ tập hợp hành vi nào cũng có thể được mô tả bằng thuộc tính bảo mật (sự an toàn) và đặc tính sống sót (sự sống động). An toàn có nghĩa là sẽ không có chuyện gì xấu xảy ra, chương trình sẽ không đưa ra đáp án sai. Khả năng sống sót có nghĩa là sớm hay muộn điều gì đó tốt đẹp sẽ xảy ra, tức là chương trình sớm hay muộn sẽ đưa ra câu trả lời chính xác. Theo quy định, bảo mật là một chỉ báo quan trọng hơn, lỗi thường xảy ra ở đây nhất. Vì vậy, để tiết kiệm thời gian, tôi sẽ không nói về khả năng sống sót, mặc dù tất nhiên nó cũng rất quan trọng.
Chúng ta đạt được sự an toàn bằng cách trước tiên chỉ định một tập hợp các trạng thái ban đầu có thể có. Và thứ hai, mối quan hệ với tất cả các trạng thái tiếp theo có thể có của mỗi trạng thái. Hãy cư xử như các nhà khoa học và xác định các trạng thái bằng toán học. Tập hợp các trạng thái ban đầu được mô tả bằng công thức, ví dụ, trong trường hợp thuật toán Euclide: (x = M) ∧ (y = N). Đối với những giá trị nhất định M и N chỉ có một trạng thái ban đầu. Mối quan hệ với trạng thái tiếp theo được mô tả bằng một công thức trong đó các biến của trạng thái tiếp theo được viết bằng số nguyên tố và các biến của trạng thái hiện tại được viết không có số nguyên tố. Trong trường hợp thuật toán Euclide, chúng ta sẽ xử lý sự phân biệt của hai công thức, trong đó một công thức x là giá trị lớn nhất, và trong giá trị thứ hai - y:
Trong trường hợp đầu tiên, giá trị mới của y bằng giá trị trước đó của y và chúng ta nhận được giá trị mới của x bằng cách trừ biến nhỏ hơn khỏi biến lớn hơn. Trong trường hợp thứ hai, chúng tôi làm ngược lại.
Hãy quay trở lại thuật toán Euclide. Giả sử một lần nữa rằng M = 12, N = 18. Điều này xác định một trạng thái ban đầu duy nhất, (x = 12) ∧ (y = 18). Sau đó, chúng tôi cắm các giá trị này vào công thức trên và nhận được:
Đây là giải pháp khả thi duy nhất: x' = 18 - 12 ∧ y' = 12, và chúng tôi nhận được hành vi: [x = 12, y = 18]. Theo cách tương tự, chúng ta có thể mô tả tất cả các trạng thái trong hành vi của mình: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].
Ở trạng thái cuối cùng [x = 6, y = 6] cả hai phần của biểu thức sẽ sai, do đó nó không có trạng thái tiếp theo. Vì vậy, chúng ta có đặc điểm kỹ thuật đầy đủ của bước thứ hai - như chúng ta thấy, đây là toán học khá bình thường, giống như toán học của các kỹ sư và nhà khoa học, và không xa lạ như trong khoa học máy tính.
Hai công thức này có thể được kết hợp thành một công thức logic thời gian. Thật tao nhã và dễ giải thích, nhưng bây giờ không có thời gian cho việc đó. Chúng ta có thể chỉ cần logic thời gian vì tính chất sống động; vì tính an toàn thì điều đó không cần thiết. Tôi không thích logic thời gian như vậy, nó không hoàn toàn là toán học thông thường, nhưng trong trường hợp sống động thì đó là một điều xấu cần thiết.
Trong thuật toán Euclide cho từng giá trị x и y có những giá trị duy nhất x' и y', điều này làm cho mối quan hệ với trạng thái tiếp theo là đúng. Nói cách khác, thuật toán Euclide có tính tất định. Để mô hình hóa một thuật toán không xác định, trạng thái hiện tại phải có nhiều trạng thái có thể xảy ra trong tương lai và mỗi giá trị của biến không có sẵn phải có nhiều giá trị của biến có sẵn sao cho mối quan hệ với trạng thái tiếp theo là đúng. Điều này không khó thực hiện, nhưng bây giờ tôi sẽ không đưa ra ví dụ.
Để tạo ra một công cụ làm việc, bạn cần có toán học hình thức. Làm thế nào để làm cho một đặc điểm kỹ thuật chính thức? Để làm điều này, chúng ta sẽ cần một ngôn ngữ chính thức, ví dụ: . Đặc tả của thuật toán Euclide trong ngôn ngữ này sẽ như sau:
Ký hiệu dấu bằng có hình tam giác nghĩa là giá trị bên trái dấu được xác định bằng giá trị bên phải dấu. Về bản chất, đặc tả là một định nghĩa, trong trường hợp của chúng ta là hai định nghĩa. Đối với đặc tả trong TLA+, bạn cần thêm các khai báo và một số cú pháp, như trong slide ở trên. Trong ASCII nó sẽ trông như thế này:
Như bạn có thể thấy, không có gì phức tạp. Thông số kỹ thuật trên TLA+ có thể được xác minh, tức là có thể bỏ qua tất cả các hành vi có thể có trong một mô hình nhỏ. Trong trường hợp của chúng tôi, mô hình này sẽ có giá trị nhất định M и N. Đây là một phương pháp xác minh rất hiệu quả và đơn giản, hoàn toàn tự động. Ngoài ra, có thể viết các bằng chứng chính thức về sự thật và kiểm tra chúng một cách máy móc, nhưng việc này tốn rất nhiều thời gian nên hầu như không ai làm việc này.
Nhược điểm chính của TLA+ là nó liên quan đến toán học, các lập trình viên và nhà khoa học máy tính đều sợ toán học. Thoạt nhìn điều này nghe có vẻ như một trò đùa, nhưng thật không may, tôi nói điều này hoàn toàn nghiêm túc. Một đồng nghiệp của tôi vừa kể cho tôi nghe cách anh ấy cố gắng giải thích TLA+ cho một số nhà phát triển. Ngay khi công thức xuất hiện trên màn hình, mắt họ lập tức trở nên đờ đẫn. Vì vậy, nếu TLA+ đáng sợ, bạn có thể sử dụng , là một loại ngôn ngữ lập trình đồ chơi. Một biểu thức trong PlusCal có thể là bất kỳ biểu thức TLA+ nào, nghĩa là về cơ bản là bất kỳ biểu thức toán học nào. Ngoài ra, PlusCal còn có cú pháp cho các thuật toán không xác định. Vì PlusCal có thể viết bất kỳ biểu thức TLA+ nào nên nó có tính biểu cảm cao hơn đáng kể so với bất kỳ ngôn ngữ lập trình thực tế nào. Tiếp theo, PlusCal được biên soạn thành thông số kỹ thuật TLA+ dễ đọc. Tất nhiên, điều này không có nghĩa là đặc tả PlusCal phức tạp sẽ trở thành đặc tả đơn giản trên TLA+ - chỉ là sự tương ứng giữa chúng là rõ ràng, sẽ không xuất hiện độ phức tạp bổ sung. Cuối cùng, thông số kỹ thuật này có thể được xác minh bằng công cụ TLA+. Nhìn chung, PlusCal có thể giúp vượt qua nỗi ám ảnh về toán học, nó dễ hiểu ngay cả đối với các lập trình viên và nhà khoa học máy tính. Trước đây tôi đã xuất bản các thuật toán về nó một thời gian (khoảng 10 năm).
Có lẽ ai đó sẽ phản đối rằng TLA+ và PlusCal là toán học và toán học chỉ hoạt động với các ví dụ bịa đặt. Trong thực tế, bạn cần một ngôn ngữ thực với các kiểu, thủ tục, đối tượng, v.v. Cái này sai. Đây là những gì Chris Newcomb, người từng làm việc tại Amazon, viết: “Chúng tôi đã sử dụng TLA+ trên mười dự án lớn và trong mọi trường hợp, việc sử dụng nó đã tạo ra sự khác biệt đáng kể cho quá trình phát triển vì chúng tôi có thể phát hiện các lỗi nguy hiểm trước khi chúng được đưa vào sản xuất và vì nó mang lại cho chúng tôi cái nhìn sâu sắc và sự tự tin mà chúng tôi cần để thực hiện tích cực. tối ưu hóa hiệu suất mà không ảnh hưởng đến tính xác thực của chương trình". Bạn có thể thường nghe rằng khi sử dụng các phương thức hình thức, chúng ta nhận được mã kém hiệu quả - trong thực tế, mọi thứ hoàn toàn ngược lại. Ngoài ra, có quan điểm cho rằng các nhà quản lý không thể bị thuyết phục về sự cần thiết của các phương pháp chính thức, ngay cả khi các lập trình viên bị thuyết phục về tính hữu ích của chúng. Và Newcomb viết: “Các nhà quản lý hiện đang cố gắng bằng mọi cách có thể để viết các thông số kỹ thuật trong TLA+ và đang phân bổ thời gian cụ thể cho việc này”. Vì vậy, khi các nhà quản lý thấy TLA+ có hiệu quả, họ sẽ đón nhận nó. Chris Newcomb đã viết điều này khoảng sáu tháng trước (tháng 2014 năm 14), nhưng hiện tại, theo như tôi biết, TLA+ được sử dụng trong 10 dự án chứ không phải 360. Một ví dụ khác liên quan đến thiết kế của XBox 360. Một thực tập sinh đã đến gặp Charles Thacker và đã viết đặc tả cho hệ thống bộ nhớ. Nhờ thông số kỹ thuật này, một lỗi đã được phát hiện mà lẽ ra không được phát hiện và có thể khiến mọi XBox XNUMX gặp sự cố sau bốn giờ sử dụng. Các kỹ sư của IBM xác nhận rằng các thử nghiệm của họ sẽ không phát hiện ra lỗi này.
Bạn có thể đọc thêm về TLA+ trên Internet, nhưng bây giờ hãy nói về các thông số kỹ thuật không chính thức. Chúng ta hiếm khi phải viết chương trình tính ước số chung nhỏ nhất và những thứ tương tự. Chúng tôi thường xuyên viết các chương trình giống như công cụ máy in đẹp mà tôi đã viết cho TLA+. Sau quá trình xử lý đơn giản nhất, mã TLA+ sẽ trông như thế này:
Nhưng trong ví dụ trên, rất có thể người dùng muốn các dấu kết hợp và dấu bằng được căn chỉnh. Vì vậy, định dạng đúng sẽ trông như thế này:
Hãy xem xét một ví dụ khác:
Ngược lại, ở đây, việc căn chỉnh các dấu bằng, phép cộng và phép nhân trong nguồn là ngẫu nhiên nên việc xử lý đơn giản nhất là khá đủ. Nói chung, không có định nghĩa toán học chính xác về định dạng chính xác, bởi vì “chính xác” trong trường hợp này có nghĩa là “điều người dùng muốn” và điều này không thể được xác định bằng toán học.
Có vẻ như nếu chúng ta không có định nghĩa về sự thật thì việc xác định nó là vô ích. Nhưng điều đó không đúng. Chỉ vì chúng ta không biết một chương trình nên làm gì không có nghĩa là chúng ta không cần nghĩ xem nó sẽ hoạt động như thế nào—ngược lại, chúng ta nên dành nhiều nỗ lực hơn nữa cho nó. Đặc điểm kỹ thuật đặc biệt quan trọng ở đây. Không thể xác định chương trình tối ưu để in có cấu trúc, nhưng điều này không có nghĩa là chúng ta hoàn toàn không nên thực hiện nó và việc viết mã như một dòng ý thức cũng không như vậy. Cuối cùng tôi đã viết một đặc tả của sáu quy tắc với các định nghĩa dưới dạng bình luận trong một tệp Java. Đây là một ví dụ về một trong những quy tắc: a left-comment token is LeftComment aligned with its covering token. Quy tắc này được viết bằng tiếng Anh toán học: LeftComment aligned, left-comment и covering token - thuật ngữ có định nghĩa. Đây là cách các nhà toán học mô tả toán học: họ viết định nghĩa của các thuật ngữ và dựa trên chúng, tạo ra các quy tắc. Lợi ích của đặc tả này là sáu quy tắc dễ hiểu và dễ gỡ lỗi hơn 850 dòng mã. Tôi phải nói rằng việc viết ra những quy tắc này không hề dễ dàng, phải mất khá nhiều thời gian để gỡ lỗi chúng. Tôi đã viết mã đặc biệt cho mục đích này để cho tôi biết quy tắc nào đang được sử dụng. Bởi vì tôi đã thử nghiệm sáu quy tắc này với một vài ví dụ nên tôi không phải gỡ lỗi 850 dòng mã và các lỗi cũng khá dễ tìm thấy. Java có những công cụ tuyệt vời cho việc này. Nếu tôi chỉ viết mã, tôi sẽ mất nhiều thời gian hơn và định dạng sẽ có chất lượng kém hơn.
Tại sao không thể sử dụng thông số kỹ thuật chính thức? Một mặt, việc thực hiện đúng ở đây không quá quan trọng. Một bản in có cấu trúc chắc chắn sẽ không làm hài lòng một số người, vì vậy tôi không cần phải làm cho nó hoạt động chính xác trong mọi tình huống bất thường. Điều quan trọng hơn nữa là tôi không có đủ công cụ. Trình kiểm tra mô hình TLA+ ở đây vô dụng nên tôi sẽ phải viết các ví dụ bằng tay.
Đặc điểm kỹ thuật nhất định có các tính năng chung cho tất cả các đặc điểm kỹ thuật. Nó ở cấp độ cao hơn mã. Nó có thể được thực hiện bằng bất kỳ ngôn ngữ nào. Không có công cụ hoặc phương pháp để viết nó. Không có khóa học lập trình nào có thể giúp bạn viết đặc tả này. Và không có công cụ nào có thể khiến thông số kỹ thuật này trở nên không cần thiết, tất nhiên trừ khi bạn đang viết một ngôn ngữ dành riêng cho việc viết các chương trình in có cấu trúc trong TLA+. Cuối cùng, thông số kỹ thuật này không nói lên điều gì về cách chúng ta viết mã chính xác như thế nào, nó chỉ cho biết mã đó làm gì. Chúng tôi viết một đặc tả để giúp chúng tôi suy nghĩ thấu đáo vấn đề trước khi bắt đầu nghĩ về mã.
Nhưng thông số kỹ thuật này cũng có những đặc điểm giúp phân biệt nó với các thông số kỹ thuật khác. 95% các thông số kỹ thuật khác ngắn hơn và đơn giản hơn nhiều:
Hơn nữa, đặc điểm kỹ thuật này là một bộ quy tắc. Đây thường là dấu hiệu của thông số kỹ thuật kém. Việc hiểu được hậu quả của một bộ quy tắc khá khó khăn, đó là lý do tại sao tôi phải dành nhiều thời gian để gỡ lỗi chúng. Tuy nhiên, trong trường hợp này tôi không thể tìm ra cách nào tốt hơn.
Điều đáng nói đôi lời về các chương trình chạy liên tục. Thông thường chúng hoạt động song song, chẳng hạn như hệ điều hành hoặc hệ thống phân tán. Rất ít người có thể hiểu được chúng trong tâm trí hoặc trên giấy tờ, và tôi không phải là một trong số họ, mặc dù tôi đã từng làm được điều đó. Do đó, chúng tôi cần các công cụ kiểm tra công việc của mình - ví dụ: TLA+ hoặc PlusCal.
Tại sao tôi cần viết đặc tả nếu tôi đã biết mã nên làm gì? Thực ra, tôi chỉ nghĩ là tôi biết điều đó. Ngoài ra, với một đặc tả đã có sẵn, người ngoài không còn cần phải xem mã để hiểu chính xác nó làm gì. Tôi có một quy tắc: không nên có quy tắc chung nào cả. Tất nhiên, có một ngoại lệ đối với quy tắc này, đây là quy tắc chung duy nhất mà tôi tuân theo: đặc tả về chức năng của mã sẽ cho mọi người biết mọi thứ họ cần biết khi sử dụng mã đó.
Vậy chính xác thì lập trình viên cần biết gì về tư duy? Trước hết, điều này cũng giống như đối với tất cả mọi người: nếu bạn không viết, thì đối với bạn, dường như bạn chỉ đang nghĩ. Ngoài ra, bạn cần suy nghĩ trước khi viết mã, điều đó có nghĩa là bạn cần viết trước khi viết mã. Đặc tả là những gì chúng ta viết trước khi bắt đầu viết mã. Bất kỳ mã nào cũng có thể được sử dụng hoặc thay đổi bởi bất kỳ ai. Và “ai đó” này có thể trở thành tác giả của đoạn mã một tháng sau khi nó được viết. Đặc tả là cần thiết cho các chương trình và hệ thống lớn, cho các lớp, cho các phương thức và đôi khi thậm chí cho các phần phức tạp của một phương thức. Chính xác thì bạn nên viết gì về mã? Bạn cần mô tả chức năng của nó, tức là thứ gì đó có thể hữu ích cho bất kỳ ai sử dụng mã này. Đôi khi cũng cần phải xác định chính xác cách mã đạt được mục tiêu. Nếu chúng ta đã học qua phương pháp này trong khóa học về thuật toán thì chúng ta gọi nó là thuật toán. Nếu nó là thứ gì đó chuyên biệt và mới mẻ hơn thì chúng tôi gọi đó là thiết kế cấp cao. Không có sự khác biệt chính thức ở đây: cả hai đều là mô hình trừu tượng của chương trình.
Bạn nên viết đặc tả mã chính xác như thế nào? Điều chính: nó phải cao hơn một cấp so với chính mã. Nó phải mô tả các trạng thái và hành vi. Nó phải nghiêm ngặt như nhiệm vụ yêu cầu. Nếu bạn đang viết đặc tả về cách triển khai một tác vụ thì nó có thể được viết bằng mã giả hoặc sử dụng PlusCal. Bạn cần học cách viết thông số kỹ thuật bằng cách sử dụng thông số kỹ thuật chính thức. Điều này sẽ cung cấp cho bạn những kỹ năng cần thiết cũng sẽ hữu ích với những kỹ năng không chính thức. Làm thế nào bạn có thể học cách viết các thông số kỹ thuật chính thức? Khi học lập trình, chúng ta viết chương trình và sau đó sửa lỗi chúng. Điều tương tự ở đây: bạn cần viết một đặc tả, kiểm tra nó bằng trình kiểm tra mô hình và sửa lỗi. TLA+ có thể không phải là ngôn ngữ tốt nhất cho thông số kỹ thuật chính thức và ngôn ngữ khác có thể phù hợp hơn với nhu cầu cụ thể của bạn. Điều tuyệt vời về TLA+ là nó làm rất tốt việc dạy tư duy toán học.
Làm thế nào để liên kết đặc tả và mã? Sử dụng các nhận xét liên kết các khái niệm toán học và cách thực hiện chúng. Nếu bạn làm việc với đồ thị thì ở cấp độ chương trình, bạn sẽ có mảng nút và mảng liên kết. Vì vậy, bạn cần phải viết chính xác cách biểu đồ được triển khai bởi các cấu trúc lập trình này.
Cần lưu ý rằng không có điều nào ở trên áp dụng cho chính quá trình viết mã. Khi viết code, tức là thực hiện bước thứ ba, bạn cũng cần phải suy nghĩ và suy nghĩ thấu đáo về chương trình. Nếu một nhiệm vụ con trở nên phức tạp hoặc không rõ ràng, bạn cần phải viết đặc tả cho nó. Nhưng tôi không nói về bản thân mã ở đây. Bạn có thể sử dụng bất kỳ ngôn ngữ lập trình nào, bất kỳ phương pháp nào, đây không phải là về chúng. Ngoài ra, không có cách nào ở trên loại bỏ nhu cầu kiểm tra và gỡ lỗi mã của bạn. Ngay cả khi mô hình trừu tượng được viết chính xác thì vẫn có thể có lỗi trong quá trình triển khai.
Viết thông số kỹ thuật là một bước bổ sung trong quá trình mã hóa. Nhờ nó, nhiều lỗi có thể được khắc phục dễ dàng hơn - chúng tôi biết điều này từ kinh nghiệm của các lập trình viên từ Amazon. Với thông số kỹ thuật, chất lượng của chương trình trở nên cao hơn. Vậy tại sao chúng ta lại thường xuyên đi mà không có chúng? Vì viết rất khó. Nhưng viết rất khó, vì để làm được điều này bạn cần phải suy nghĩ, và việc suy nghĩ cũng rất khó. Giả vờ như bạn đang suy nghĩ luôn dễ dàng hơn. Ở đây có thể rút ra một sự tương tự với việc chạy - bạn càng chạy ít thì bạn càng chạy chậm. Bạn cần rèn luyện cơ bắp và luyện viết. Nó cần thực hành.
Thông số kỹ thuật có thể không chính xác. Bạn có thể đã mắc sai lầm ở đâu đó, hoặc các yêu cầu có thể đã thay đổi hoặc có thể cần phải thực hiện một cải tiến. Bất kỳ mã nào mà bất cứ ai sử dụng đều phải thay đổi, sớm hay muộn thông số kỹ thuật sẽ không còn phù hợp với chương trình. Lý tưởng nhất là trong trường hợp này, bạn cần viết một đặc tả mới và viết lại mã hoàn toàn. Chúng tôi biết rất rõ rằng không ai làm điều này. Trong thực tế, chúng tôi vá mã và có thể cập nhật thông số kỹ thuật. Nếu điều này sớm hay muộn chắc chắn sẽ xảy ra thì tại sao lại phải viết thông số kỹ thuật? Đầu tiên, đối với người sẽ chỉnh sửa mã của bạn, mỗi từ bổ sung trong đặc tả sẽ có giá trị bằng vàng và người này rất có thể là bạn. Tôi thường tự trách mình vì không đủ cụ thể khi chỉnh sửa mã của mình. Và tôi viết nhiều thông số kỹ thuật hơn là viết mã. Vì vậy, khi bạn chỉnh sửa mã, thông số kỹ thuật luôn cần được cập nhật. Thứ hai, sau mỗi lần chỉnh sửa, mã sẽ trở nên tệ hơn, khó đọc và bảo trì hơn. Đây là sự gia tăng entropy. Nhưng nếu bạn không bắt đầu với thông số kỹ thuật thì mỗi dòng bạn viết sẽ là một bản chỉnh sửa và mã sẽ cồng kềnh và khó đọc ngay từ đầu.
Như đã nói , không trận chiến nào thắng theo kế hoạch và không trận chiến nào thắng mà không có kế hoạch. Và anh ấy biết điều gì đó về các trận chiến. Có ý kiến cho rằng viết thông số kỹ thuật là lãng phí thời gian. Đôi khi điều này đúng và nhiệm vụ quá đơn giản đến mức không cần phải suy nghĩ kỹ càng. Nhưng bạn nên luôn nhớ rằng khi bạn được khuyên không nên viết thông số kỹ thuật, điều đó có nghĩa là bạn được khuyên không nên suy nghĩ. Và bạn nên nghĩ về điều này mọi lúc. Suy nghĩ thấu đáo về một nhiệm vụ không đảm bảo rằng bạn sẽ không mắc sai lầm. Như chúng ta biết, không ai phát minh ra cây đũa thần và lập trình là một công việc khó khăn. Nhưng nếu bạn không suy nghĩ thấu đáo về nhiệm vụ, bạn chắc chắn sẽ mắc sai lầm.
Bạn có thể đọc thêm về TLA+ và PlusCal trên một trang web đặc biệt, bạn có thể truy cập vào đó từ trang chủ của tôi . Đó là tất cả đối với tôi, cảm ơn sự quan tâm của bạn.
Hãy nhớ rằng đây là một bản dịch. Khi bạn viết bình luận, hãy nhớ rằng tác giả sẽ không đọc chúng. Nếu bạn thực sự muốn trò chuyện với tác giả, anh ấy sẽ có mặt tại hội nghị Hydra 2019, được tổ chức vào ngày 11-12 tháng 2019 năm XNUMX tại St. Petersburg. Có thể mua vé .
Nguồn: www.habr.com