15: Coding với lý luận

Cố gắng lý luận về tính chính xác của phần mềm bằng tay dẫn đến một bằng chứng chính thức còn dài hơn cả code và có khả năng chứa nhiều lỗi hơn. Công cụ tự động thích hợp, nhưng không phải lúc nào cũng khả thi. Những điều sau đây mô tả một vấn đề: lý luận bán chính thức về tính đúng đắn.

Cách tiếp cận cơ bản là chia tất cả các code cần được xem xét thành các phần nhỏ- từ một dòng duy nhất, chẳng hạn một function call, cho đến những đoạn có ít hơn mười dòng- và tranh luận về tính chính xác của chúng. Cuộc tranh luận chỉ cần đủ mạnh để thuyết phục người bạn lập trình viên ủng- hộ- sự- bào- chữa- của- quỷ.

Một section nên được chọn sao cho tại mỗi điểm cuối, trạng thái của chương trình (cụ thể là bộ đếm chương trình và giá trị của các đối tượng) thỏa mãn thuộc tính được mô tả. Và chức năng của nó (chuyển đổi trạng thái) có thể dễ dàng mô tả một nhiệm vụ duy nhất. Những điều này sẽ giúp cho lý luận trở nên đơn giản hơn. Các thuộc tính như vậy khái quát các khái niệm như điều kiện tiên quyết và hậu điều kiện cho các hàm và bất biến cho các vòng lặp và class (với sự tôn trọng các trường hợp của chúng). Cố gắng để các section độc lập với nhau giúp đơn giản hóa lý luận và là điều không thể thiếu khi cần sửa đổi.

Nhiều thực hành coding nổi tiếng (mặc dù có lẽ ít được theo dõi) và được coi là “tốt” sẽ giúp cho việc suy luận trở nên dễ dàng hơn. Do đó, chỉ bằng cách có dự định về những lý luận cho code của bạn, bạn đã bắt đầu suy nghĩ về một phong cách và cấu trúc tốt hơn. Không có gì đáng ngạc nhiên, hầu hết các thực hành này có thể được kiểm tra bằng các máy phân tích code tĩnh:

• Tránh sử dụng các câu lệnh goto, vì chúng làm cho các section phụ thuộc lẫn nhau quá nhiều.
• Tránh sử dụng các biến toàn cục có thể sửa đổi, vì sẽ dẫn đến các section liên quan phụ thuộc vào chúng.
• Mỗi biến nên có phạm vi nhỏ nhất có thể. Ví dụ, một đối tượng cục bộ có thể được khai báo ngay trước khi sử dụng lần đầu.
• Làm cho các đối tượng bất biến bất cứ khi nào có liên quan.
• Làm cho code trở nên dễ đọc bằng cách sử dụng khoảng cách, cả ngang và dọc. Ví dụ: căn chỉnh các cấu trúc liên quan và sử dụng một dòng trống để phân biệt hai phần riêng.
• Làm cho code tự ghi chú lại bằng cách chọn tên mô tả (nhưng tương đối ngắn) cho các đối tượng, loại, hàm, v.v.
• Nếu bạn cần nested section, hãy cho nó một function.
• Làm cho các chức năng của bạn ngắn và tập trung vào một nhiệm vụ duy nhất. Áp dụng giới hạn 24 dòng. Mặc dù kích thước và độ phân giải màn hình đã thay đổi, nhưng không có gì thay đổi trong nhận thức của con người kể từ những năm 1960.
• Các hàm nên có ít tham số (bốn là giới hạn tốt nhất). Điều này không hạn chế dữ liệu được truyền đến các hàm: Gộp các tham số liên quan vào chung một đối tượng thu lợi từ các đối tượng bất biến và lý luận, chẳng hạn như sự gắn kết và tính nhất quán của chúng.
• Tổng quát hơn, mỗi đơn vị code, từ một đoạn đến cả thư viện, nên có một giao diện hẹp. Ít giao tiếp giảm lượng lý luận cần thiết. Điều này có nghĩa là các getter trả lại trạng thái nội bộ là một trách nhiệm pháp lý. Đừng yêu cầu đối tượng cung cấp thông tin để làm việc; thay vào đó, hãy yêu cầu đối tượng thực hiện công việc với thông tin đã có. Nói cách khác, đóng gói là tất cả về giao diện hẹp.
• Để duy trì các class bất biến, việc sử dụng các setter nên được khuyến khích, vì các setter có xu hướng cho phép các bất biến chi phối trạng thái của một đối tượng bị phá vỡ.

Cũng như lý luận về tính đúng đắn, tranh luận về code giúp bạn hiểu thêm về nó. Truyền đạt những hiểu biết bạn có vì lợi ích của mọi người.