การเขียนโปรแกรมเป็นมากกว่าการเข้ารหัส

นี่คือบทความแปล สัมมนาสแตนฟอร์ด. แต่ก่อนหน้านั้นก็มีการแนะนำสั้นๆ ซอมบี้เกิดขึ้นได้อย่างไร? ทุกคนพบว่าตัวเองอยู่ในสถานการณ์ที่ต้องการยกระดับเพื่อนหรือเพื่อนร่วมงานให้อยู่ในระดับของตัวเอง แต่ก็ไม่ได้ผล ยิ่งกว่านั้น "มันไม่ได้ผล" สำหรับคุณ แต่สำหรับเขาในด้านหนึ่งมีเงินเดือนปกติ งานและอื่น ๆ และอีกด้านหนึ่งคือต้องคิด การคิดนั้นไม่เป็นที่พอใจและเจ็บปวด เขายอมแพ้อย่างรวดเร็วและเขียนโค้ดต่อไปโดยไม่ใช้สมองเลย คุณตระหนักดีว่าต้องใช้ความพยายามมากเพียงใดเพื่อเอาชนะอุปสรรคของการไร้ประโยชน์ในการเรียนรู้ และคุณไม่ได้ทำเลย นี่คือวิธีที่ซอมบี้เกิดขึ้นซึ่งดูเหมือนจะรักษาได้ แต่ดูเหมือนว่าจะไม่มีใครทำเช่นนี้

เมื่อฉันเห็นสิ่งนั้น เลสลี่ แลมพอร์ต (ใช่แล้ว เพื่อนคนเดียวกันจากหนังสือเรียน) มาถึงรัสเซีย และไม่ได้รายงานแต่เป็นช่วงถาม-ตอบ ผมค่อนข้างจะระวังนิดหน่อย ในกรณีนี้ เลสลีเป็นนักวิทยาศาสตร์ที่มีชื่อเสียงระดับโลก เป็นผู้เขียนผลงานอันทรงคุณค่าในด้านคอมพิวเตอร์แบบกระจาย และคุณอาจรู้จักเขาด้วยตัวอักษร La ใน LaTeX - “Lamport TeX” ปัจจัยที่น่าตกใจประการที่สองคือข้อกำหนดของเขา: ทุกคนที่มาจะต้องฟังรายงานของเขาล่วงหน้า (โดยไม่เสียค่าใช้จ่ายใดๆ ทั้งสิ้น) ตั้งคำถามอย่างน้อยหนึ่งคำถามเกี่ยวกับรายงานเหล่านั้น จากนั้นจึงมาเท่านั้น ฉันตัดสินใจว่าจะดูว่าแลมพอร์ตออกอากาศรายการอะไรที่นั่น - และมันเยี่ยมมาก! นี่แหละคือยาวิเศษสำหรับรักษาซอมบี้ ฉันขอเตือนคุณว่า ข้อความนี้อาจทำให้ผู้ที่ชื่นชอบวิธีการแบบคล่องตัวขั้นสุดยอดและผู้ไม่ชอบทดสอบสิ่งที่พวกเขาเขียนอาจทำให้ใจสลายได้

หลังจากฮาโบรคัต การแปลของการสัมมนาก็เริ่มต้นขึ้นจริงๆ สนุกกับการอ่าน!

ไม่ว่าคุณจะทำงานอะไร คุณต้องทำตามสามขั้นตอนเสมอ:

• ตัดสินใจว่าเป้าหมายใดที่คุณต้องการบรรลุ
• ตัดสินใจว่าคุณจะบรรลุเป้าหมายได้อย่างไร
• บรรลุเป้าหมายของคุณ

นอกจากนี้ยังใช้กับการเขียนโปรแกรมด้วย เมื่อเราเขียนโค้ดเราต้องการ:

• ตัดสินใจว่าโปรแกรมควรทำอะไร
• กำหนดอย่างชัดเจนว่าควรปฏิบัติงานอย่างไร
• เขียนโค้ดที่เหมาะสม

แน่นอนว่าขั้นตอนสุดท้ายสำคัญมาก แต่ฉันจะไม่พูดถึงมันในวันนี้ เราจะพูดถึงสองเรื่องแรกแทน โปรแกรมเมอร์ทุกคนดำเนินการก่อนเริ่มทำงาน คุณไม่ต้องนั่งลงเพื่อเขียน เว้นแต่คุณจะตัดสินใจว่าคุณกำลังเขียนอะไร: เบราว์เซอร์หรือฐานข้อมูล ต้องมีแนวคิดบางอย่างเกี่ยวกับเป้าหมาย และคุณคิดอย่างแน่นอนว่าโปรแกรมจะทำอะไรกันแน่ และอย่าเขียนมันอย่างไม่ได้ตั้งใจด้วยความหวังว่าโค้ดจะกลายเป็นเบราว์เซอร์

การคิดโค้ดล่วงหน้านี้เกิดขึ้นได้อย่างไร? เราควรทุ่มเทความพยายามมากแค่ไหน? ทุกอย่างขึ้นอยู่กับความซับซ้อนของปัญหาที่เรากำลังแก้ไข สมมติว่าเราต้องการเขียนระบบแบบกระจายที่ทนทานต่อข้อผิดพลาด ในกรณีนี้ เราควรคิดให้รอบคอบก่อนจะนั่งเขียนโค้ด จะเป็นอย่างไรหากเราต้องการเพิ่มตัวแปรจำนวนเต็มขึ้น 1? เมื่อมองแวบแรก ทุกอย่างที่นี่เป็นเรื่องเล็กน้อยและไม่จำเป็นต้องคิด แต่แล้วเราก็จำได้ว่าอาจเกิดการล้นได้ ดังนั้น แม้เพื่อที่จะเข้าใจว่าปัญหานั้นง่ายหรือซับซ้อน คุณก็ต้องคิดก่อน

หากคุณคิดหาวิธีแก้ไขปัญหาที่เป็นไปได้ล่วงหน้า คุณสามารถหลีกเลี่ยงข้อผิดพลาดได้ แต่สิ่งนี้ต้องการให้ความคิดของคุณชัดเจน เพื่อให้บรรลุเป้าหมายนี้ คุณต้องเขียนความคิดของคุณลงไป ฉันชอบคำพูดของ Dick Guindon ที่ว่า “เมื่อคุณเขียน ธรรมชาติจะแสดงให้คุณเห็นว่าความคิดของคุณเลอะเทอะเพียงใด” ถ้าไม่เขียนก็คิดแต่ว่ากำลังคิดอยู่ และคุณต้องเขียนความคิดของคุณในรูปแบบของข้อกำหนด

ข้อมูลจำเพาะรองรับการใช้งานได้หลายอย่าง โดยเฉพาะในโครงการขนาดใหญ่ แต่ฉันจะพูดถึงแค่เรื่องเดียวเท่านั้น: มันช่วยให้เราคิดได้ชัดเจน การคิดให้ชัดเจนเป็นสิ่งสำคัญมากและค่อนข้างยาก ดังนั้นเราจึงต้องการความช่วยเหลือที่นี่ เราควรเขียนข้อกำหนดเป็นภาษาใด โดยทั่วไปนี่เป็นคำถามแรกสำหรับโปรแกรมเมอร์เสมอ: เราจะเขียนเป็นภาษาอะไร? ไม่มีคำตอบที่ถูกต้อง: ปัญหาที่เราแก้ไขนั้นหลากหลายเกินไป สำหรับบางคน TLA+ เป็นภาษาข้อกำหนดที่ฉันพัฒนาขึ้น สำหรับคนอื่นๆ การใช้ภาษาจีนจะสะดวกกว่า ทุกอย่างขึ้นอยู่กับสถานการณ์

คำถามที่สำคัญกว่านั้นคือ เราจะบรรลุการคิดที่ชัดเจนยิ่งขึ้นได้อย่างไร คำตอบ: เราต้องคิดเหมือนนักวิทยาศาสตร์ นี่เป็นวิธีคิดที่ได้ผลดีตลอด 500 ปีที่ผ่านมา ในทางวิทยาศาสตร์ เราสร้างแบบจำลองทางคณิตศาสตร์ของความเป็นจริง ดาราศาสตร์อาจเป็นศาสตร์แรกในความหมายที่เข้มงวดของคำนี้ ในแบบจำลองทางคณิตศาสตร์ที่ใช้ในดาราศาสตร์ เทห์ฟากฟ้าจะปรากฏเป็นจุดที่มีมวล ตำแหน่ง และโมเมนตัม แม้ว่าในความเป็นจริงแล้ว เทห์ฟากฟ้าจะเป็นวัตถุที่ซับซ้อนอย่างยิ่ง โดยมีภูเขา มหาสมุทร มีน้ำลงและกระแสน้ำ โมเดลนี้ถูกสร้างขึ้นเพื่อแก้ไขปัญหาบางอย่างเช่นเดียวกับรุ่นอื่น ๆ เป็นการดีในการพิจารณาว่าจะชี้กล้องโทรทรรศน์ไปที่ใดหากคุณต้องการค้นหาดาวเคราะห์ แต่ถ้าคุณต้องการพยากรณ์อากาศบนโลกใบนี้ โมเดลนี้จะไม่ทำงาน

คณิตศาสตร์ช่วยให้เราสามารถกำหนดคุณสมบัติของแบบจำลองได้ และวิทยาศาสตร์แสดงให้เห็นว่าคุณสมบัติเหล่านี้เกี่ยวข้องกับความเป็นจริงอย่างไร เรามาพูดถึงวิทยาศาสตร์ของเรา วิทยาการคอมพิวเตอร์กันดีกว่า ความจริงที่เราร่วมงานด้วยคือระบบคอมพิวเตอร์หลายประเภท เช่น โปรเซสเซอร์ เครื่องเล่นเกม คอมพิวเตอร์ที่ใช้รันโปรแกรม และอื่นๆ ฉันจะพูดถึงการรันโปรแกรมบนคอมพิวเตอร์ แต่โดยส่วนใหญ่แล้วข้อสรุปทั้งหมดนี้ใช้กับระบบคอมพิวเตอร์ใด ๆ ในทางวิทยาศาสตร์ของเรา เราใช้โมเดลที่แตกต่างกันมากมาย เช่น เครื่องจักรทัวริง ชุดเหตุการณ์ที่เรียงลำดับบางส่วน และอื่นๆ อีกมากมาย

โปรแกรมคืออะไร? นี่คือรหัสใด ๆ ที่สามารถพิจารณาได้ด้วยตัวเอง สมมติว่าเราจำเป็นต้องเขียนเบราว์เซอร์ เราดำเนินการสามงาน: ออกแบบการนำเสนอโปรแกรมของผู้ใช้ จากนั้นเขียนไดอะแกรมระดับสูงของโปรแกรม และสุดท้ายเขียนโค้ด ขณะที่เราเขียนโค้ด เราตระหนักดีว่าเราต้องเขียนตัวจัดรูปแบบข้อความ อีกครั้งเราต้องแก้ไขปัญหาสามประการ: กำหนดว่าเครื่องมือนี้จะส่งคืนข้อความใด เลือกอัลกอริทึมสำหรับการจัดรูปแบบ เขียนโค้ด งานนี้มีงานย่อยของตัวเอง: การใส่ยัติภังค์ลงในคำอย่างถูกต้อง เรายังแก้ไขงานย่อยนี้ในสามขั้นตอน - ดังที่เราเห็น งานย่อยนี้ถูกทำซ้ำในหลายระดับ

มาดูขั้นตอนแรกให้ละเอียดยิ่งขึ้น: โปรแกรมแก้ปัญหาอะไรได้บ้าง ในที่นี้เรามักจะจำลองโปรแกรมเป็นฟังก์ชันที่รับอินพุตบางส่วนและให้เอาต์พุตบางส่วน ในทางคณิตศาสตร์ ฟังก์ชันมักจะอธิบายว่าเป็นชุดคู่เรียงลำดับ ตัวอย่างเช่น ฟังก์ชันกำลังสองสำหรับจำนวนธรรมชาติจะอธิบายเป็นเซต {<0,0>, <1,1>, <2,4>, <3,9>, …} ขอบเขตของคำจำกัดความของฟังก์ชันดังกล่าวคือเซตขององค์ประกอบแรกของแต่ละคู่ ซึ่งก็คือจำนวนธรรมชาติ ในการกำหนดฟังก์ชัน เราต้องระบุโดเมนและสูตรของมัน

แต่ฟังก์ชันทางคณิตศาสตร์ไม่เหมือนกับฟังก์ชันในภาษาโปรแกรม คณิตศาสตร์นั้นง่ายกว่ามาก เนื่องจากฉันไม่มีเวลาสำหรับตัวอย่างที่ซับซ้อน ลองพิจารณาตัวอย่างง่ายๆ กัน: ฟังก์ชันในภาษา C หรือวิธีคงที่ใน Java ที่ส่งคืนตัวหารร่วมมากที่สุดของจำนวนเต็มสองตัว ในข้อกำหนดของวิธีนี้เราจะเขียนว่า: คำนวณ GCD(M,N) สำหรับการโต้แย้ง M и Nที่ไหน GCD(M,N) - ฟังก์ชันที่มีโดเมนเป็นชุดของคู่ของจำนวนเต็ม และค่าที่ส่งคืนคือจำนวนเต็มที่ใหญ่ที่สุดที่หารด้วย M и N. ความเป็นจริงเปรียบเทียบกับรุ่นนี้เป็นอย่างไร? โมเดลทำงานด้วยจำนวนเต็ม และใน C หรือ Java เรามี 32 บิต int. โมเดลนี้ช่วยให้เราตัดสินใจได้ว่าอัลกอริทึมนั้นถูกต้องหรือไม่ GCDแต่จะไม่ป้องกันข้อผิดพลาดล้น สิ่งนี้จะต้องมีแบบจำลองที่ซับซ้อนมากขึ้นซึ่งไม่มีเวลา

เรามาพูดถึงข้อจำกัดของฟังก์ชันในฐานะโมเดลกันดีกว่า บางโปรแกรม (เช่น ระบบปฏิบัติการ) ไม่เพียงแต่คืนค่าเฉพาะสำหรับอาร์กิวเมนต์บางตัวเท่านั้น แต่ยังสามารถทำงานได้อย่างต่อเนื่อง นอกจากนี้ ฟังก์ชันที่เป็นแบบจำลองไม่เหมาะกับขั้นตอนที่สอง นั่นคือการวางแผนวิธีแก้ปัญหา Quicksort และ Bubble sort คำนวณฟังก์ชันเดียวกัน แต่เป็นอัลกอริธึมที่แตกต่างกันโดยสิ้นเชิง ดังนั้นเพื่ออธิบายวิธีการบรรลุเป้าหมายของโปรแกรมผมจึงใช้โมเดลอื่นเรียกว่าโมเดลพฤติกรรมมาตรฐาน โปรแกรมจะแสดงเป็นชุดของพฤติกรรมที่ถูกต้องทั้งหมด ซึ่งแต่ละพฤติกรรมตามลำดับจะเป็นลำดับของสถานะ และสถานะจะเป็นการกำหนดค่าให้กับตัวแปร

มาดูกันว่าขั้นตอนที่สองของอัลกอริทึมแบบยุคลิดจะเป็นอย่างไร เราจำเป็นต้องคำนวณ GCD(M, N). เราเริ่มต้น M ในขณะที่ xและ N ในขณะที่ yแล้วลบตัวแปรที่น้อยกว่าออกจากตัวแปรที่ใหญ่กว่าซ้ำๆ กันจนกว่าจะเท่ากัน ตัวอย่างเช่น ถ้า M = 12และ N = 18เราสามารถอธิบายพฤติกรรมต่อไปนี้:

[x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6]

และถ้าหาก M = 0 и N = 0? XNUMX หารด้วยตัวเลขทุกตัวลงตัว ในกรณีนี้จึงไม่มีตัวหารที่มากที่สุด ในสถานการณ์นี้ เราต้องกลับไปที่ขั้นตอนแรกแล้วถามว่า เราจำเป็นต้องคำนวณ GCD สำหรับตัวเลขที่ไม่เป็นบวกจริงหรือ หากไม่จำเป็น คุณเพียงแค่ต้องเปลี่ยนข้อมูลจำเพาะเท่านั้น

การพูดนอกเรื่องสั้น ๆ เกี่ยวกับประสิทธิภาพการผลิตเป็นไปตามลำดับที่นี่ มักวัดจากจำนวนบรรทัดของโค้ดที่เขียนต่อวัน แต่งานของคุณจะมีประโยชน์มากขึ้นหากคุณกำจัดบรรทัดจำนวนหนึ่งออกไป เนื่องจากคุณมีพื้นที่สำหรับข้อบกพร่องน้อยลง และวิธีที่ง่ายที่สุดในการกำจัดโค้ดคือในขั้นตอนแรก เป็นไปได้ว่าคุณไม่ต้องการสิ่งกระตุ้นทั้งหมดที่คุณพยายามจะนำไปใช้ วิธีที่เร็วที่สุดในการลดความซับซ้อนของโปรแกรมและประหยัดเวลาคือการไม่ทำสิ่งที่ไม่ควรทำ ขั้นตอนที่สองมีศักยภาพในการประหยัดเวลาสูงสุดเป็นอันดับสอง หากคุณวัดประสิทธิภาพการทำงานในแง่ของบรรทัดที่เขียน การคิดถึงวิธีทำงานให้สำเร็จจะทำให้คุณ มีประสิทธิผลน้อยลงเพราะคุณสามารถแก้ไขปัญหาเดียวกันได้โดยใช้โค้ดน้อยลง ฉันไม่สามารถให้สถิติที่แน่นอนได้ที่นี่ เนื่องจากฉันไม่สามารถนับจำนวนบรรทัดที่ฉันไม่ได้เขียนเนื่องจากเวลาที่ฉันใช้ไปกับข้อกำหนด นั่นคือในขั้นตอนแรกและขั้นตอนที่สอง และเราไม่สามารถทำการทดลองที่นี่ได้เช่นกัน เนื่องจากในการทดสอบเราไม่มีสิทธิ์ทำขั้นตอนแรกให้เสร็จสิ้น งานจะถูกกำหนดไว้ล่วงหน้า

เป็นเรื่องง่ายที่จะมองข้ามปัญหาต่างๆ ในข้อกำหนดที่ไม่เป็นทางการ การเขียนข้อกำหนดที่เข้มงวดสำหรับฟังก์ชันต่างๆ ไม่ใช่เรื่องยาก ฉันจะไม่พูดถึงเรื่องนี้ เราจะพูดถึงการเขียนข้อกำหนดที่เข้มงวดสำหรับพฤติกรรมมาตรฐานแทน มีทฤษฎีบทที่ระบุว่าชุดพฤติกรรมใดๆ สามารถอธิบายได้โดยใช้คุณสมบัติความปลอดภัย (ความปลอดภัย) และคุณสมบัติการอยู่รอด (ความมีชีวิตชีวา). ความปลอดภัยหมายความว่าจะไม่มีอะไรเลวร้ายเกิดขึ้น โปรแกรมจะไม่ให้คำตอบที่ผิด ความอยู่รอดหมายความว่าไม่ช้าก็เร็วสิ่งดีๆ จะเกิดขึ้น เช่น โปรแกรมจะให้คำตอบที่ถูกต้องไม่ช้าก็เร็ว ตามกฎแล้วความปลอดภัยเป็นตัวบ่งชี้ที่สำคัญกว่า ข้อผิดพลาดมักเกิดขึ้นที่นี่ ดังนั้นเพื่อเป็นการประหยัดเวลา ฉันจะไม่พูดถึงความอยู่รอด ถึงแม้ว่าแน่นอนว่ามันก็สำคัญเช่นกัน

เราบรรลุความปลอดภัยโดยการระบุชุดของสถานะเริ่มต้นที่เป็นไปได้ก่อน และประการที่สอง ความสัมพันธ์กับสถานะถัดไปที่เป็นไปได้ทั้งหมดสำหรับแต่ละรัฐ มาทำตัวเหมือนนักวิทยาศาสตร์และกำหนดสถานะทางคณิตศาสตร์กันเถอะ เซตของสถานะเริ่มต้นอธิบายไว้ในสูตร ตัวอย่างเช่น ในกรณีของอัลกอริทึมแบบยุคลิด: (x = M) ∧ (y = N). สำหรับค่าบางอย่าง M и N มีสถานะเริ่มต้นเพียงสถานะเดียวเท่านั้น ความสัมพันธ์กับสถานะถัดไปอธิบายได้ด้วยสูตรที่ตัวแปรของสถานะถัดไปเขียนด้วยจำนวนเฉพาะ และตัวแปรของสถานะปัจจุบันเขียนโดยไม่มีจำนวนเฉพาะ ในกรณีของอัลกอริทึมแบบยุคลิด เราจะจัดการกับการแยกกันของสูตรสองสูตร โดยหนึ่งในนั้น x เป็นค่าที่ใหญ่ที่สุด และในวินาที - y:

ในกรณีแรก ค่าใหม่ของ y เท่ากับค่า y ก่อนหน้า และเราจะได้ค่าใหม่ของ x โดยการลบตัวแปรที่น้อยกว่าออกจากตัวแปรที่ใหญ่กว่า ในกรณีที่สอง เราทำตรงกันข้าม

กลับไปที่อัลกอริทึมแบบยุคลิดกัน สมมุติอีกครั้งว่า M = 12, N = 18. สิ่งนี้กำหนดสถานะเริ่มต้นเดียว (x = 12) ∧ (y = 18). จากนั้นเราเสียบค่าเหล่านี้ลงในสูตรด้านบนและรับ:

นี่เป็นทางออกเดียวที่เป็นไปได้: x' = 18 - 12 ∧ y' = 12และเราได้รับพฤติกรรม: [x = 12, y = 18]. ในทำนองเดียวกัน เราสามารถอธิบายสถานะทั้งหมดในพฤติกรรมของเราได้: [x = 12, y = 18] → [x = 12, y = 6] → [x = 6, y = 6].

ในสถานะสุดท้าย [x = 6, y = 6] ทั้งสองส่วนของนิพจน์จะเป็นเท็จ ดังนั้นจึงไม่มีสถานะถัดไป ดังนั้นเราจึงมีข้อกำหนดที่สมบูรณ์ของขั้นตอนที่สอง ดังที่เราเห็น นี่เป็นคณิตศาสตร์ที่ค่อนข้างธรรมดา เหมือนกับของวิศวกรและนักวิทยาศาสตร์ และไม่แปลก เหมือนในวิทยาการคอมพิวเตอร์

สองสูตรนี้สามารถรวมกันเป็นสูตรหนึ่งของตรรกะชั่วคราวได้ มันสวยงามและอธิบายง่าย แต่ตอนนี้ไม่มีเวลาแล้ว เราอาจต้องใช้ตรรกะชั่วคราวเพื่อคุณสมบัติของความมีชีวิตชีวาเท่านั้น เพื่อความปลอดภัยไม่จำเป็น ฉันไม่ชอบตรรกะชั่วคราวเช่นนี้ มันไม่ใช่คณิตศาสตร์ธรรมดาๆ แต่ในกรณีของความมีชีวิตชีวา มันเป็นสิ่งชั่วร้ายที่จำเป็น

ในอัลกอริทึมแบบยุคลิดสำหรับแต่ละค่า x и y มีคุณค่าที่ไม่ซ้ำใคร x' и y'ซึ่งทำให้ความสัมพันธ์กับสถานะถัดไปเป็นจริง กล่าวอีกนัยหนึ่ง อัลกอริธึมแบบยุคลิดเป็นแบบกำหนดได้ ในการสร้างแบบจำลองอัลกอริธึมแบบไม่กำหนดไว้ สถานะปัจจุบันจะต้องมีสถานะในอนาคตที่เป็นไปได้หลายค่า และแต่ละค่าของตัวแปรที่ไม่ได้กำหนดไว้จะต้องมีค่าของตัวแปรที่เตรียมไว้หลายค่า เพื่อให้ความสัมพันธ์กับสถานะถัดไปเป็นจริง นี่ไม่ใช่เรื่องยาก แต่ฉันจะไม่ยกตัวอย่างตอนนี้

ในการสร้างเครื่องมือที่ใช้งานได้คุณต้องมีคณิตศาสตร์ที่เป็นทางการ จะทำข้อกำหนดอย่างเป็นทางการได้อย่างไร? ในการดำเนินการนี้ เราจำเป็นต้องมีภาษาที่เป็นทางการ เช่น ส.ส.ท.+. ข้อมูลจำเพาะของอัลกอริทึมแบบยุคลิดในภาษานี้จะมีลักษณะดังนี้:

สัญลักษณ์เครื่องหมายเท่ากับรูปสามเหลี่ยมหมายความว่าค่าทางด้านซ้ายของเครื่องหมายถูกกำหนดให้เท่ากับค่าทางด้านขวาของเครื่องหมาย โดยพื้นฐานแล้ว ข้อกำหนดคือคำจำกัดความ ในกรณีของเรามีคำจำกัดความสองแบบ ในข้อกำหนดใน TLA+ คุณต้องเพิ่มการประกาศและไวยากรณ์บางอย่าง ดังในสไลด์ด้านบน ใน ASCII จะมีลักษณะดังนี้:

อย่างที่คุณเห็นไม่มีอะไรซับซ้อน สามารถทดสอบข้อกำหนดบน TLA+ ได้ กล่าวคือ พฤติกรรมที่เป็นไปได้ทั้งหมดสามารถประเมินได้ในแบบจำลองขนาดเล็ก ในกรณีของเรา โมเดลนี้จะเป็นค่าที่แน่นอน M и N. นี่เป็นวิธีการตรวจสอบที่มีประสิทธิภาพและง่ายดายซึ่งเป็นไปโดยอัตโนมัติโดยสมบูรณ์ นอกจากนี้ เป็นไปได้ที่จะเขียนการพิสูจน์ความจริงอย่างเป็นทางการและตรวจสอบโดยกลไก แต่การดำเนินการนี้ใช้เวลานาน ดังนั้นจึงแทบไม่มีใครทำเช่นนี้

ข้อเสียเปรียบหลักของ TLA+ คือมันเป็นคณิตศาสตร์ ส่วนโปรแกรมเมอร์และนักวิทยาศาสตร์คอมพิวเตอร์ก็กลัวคณิตศาสตร์ เมื่อมองแวบแรกดูเหมือนเป็นเรื่องตลก แต่น่าเสียดายที่ฉันพูดแบบนี้อย่างจริงจัง เพื่อนร่วมงานของฉันเพิ่งบอกฉันว่าเขาพยายามอธิบาย TLA+ ให้กับนักพัฒนาหลายคนอย่างไร ทันทีที่สูตรปรากฏบนหน้าจอ ดวงตาของพวกเขาก็กลายเป็นแก้วทันที ดังนั้นหาก TLA+ น่ากลัว คุณสามารถใช้ได้ พลัสแคลเป็นภาษาโปรแกรมของเล่นชนิดหนึ่ง นิพจน์ใน PlusCal อาจเป็นนิพจน์ TLA+ ใดก็ได้ กล่าวคือ โดยพื้นฐานแล้วคือนิพจน์ทางคณิตศาสตร์ใดก็ได้ นอกจากนี้ PlusCal ยังมีไวยากรณ์สำหรับอัลกอริทึมที่ไม่สามารถกำหนดได้ เนื่องจาก PlusCal สามารถเขียนนิพจน์ TLA+ ใดๆ ได้ จึงมีการแสดงออกมากกว่าภาษาการเขียนโปรแกรมจริงใดๆ อย่างมาก จากนั้น PlusCal จะถูกรวบรวมเป็นข้อกำหนด TLA+ ที่อ่านง่าย แน่นอนว่านี่ไม่ได้หมายความว่าข้อกำหนด PlusCal ที่ซับซ้อนจะกลายเป็นข้อกำหนดธรรมดาบน TLA+ เพียงแต่มีความสอดคล้องกันระหว่างข้อกำหนดเหล่านั้นอย่างชัดเจน และจะไม่มีความซับซ้อนเพิ่มเติมใดๆ เกิดขึ้น สุดท้ายนี้ สามารถตรวจสอบข้อกำหนดนี้ได้โดยใช้เครื่องมือ TLA+ โดยทั่วไป PlusCal สามารถช่วยเอาชนะความหวาดกลัวทางคณิตศาสตร์ได้ ซึ่งเป็นเรื่องง่ายที่จะเข้าใจแม้กระทั่งสำหรับโปรแกรมเมอร์และนักวิทยาศาสตร์คอมพิวเตอร์ ฉันเผยแพร่อัลกอริธึมเกี่ยวกับมันมาระยะหนึ่งแล้ว (ประมาณ 10 ปี) ในอดีต

บางทีบางคนอาจแย้งว่า TLA+ และ PlusCal เป็นคณิตศาสตร์ และคณิตศาสตร์ใช้ได้กับตัวอย่างที่สร้างขึ้นเท่านั้น ในทางปฏิบัติ คุณจำเป็นต้องมีภาษาจริงพร้อมประเภท ขั้นตอน วัตถุ และอื่นๆ นี่เป็นสิ่งที่ผิด นี่คือสิ่งที่ Chris Newcomb ซึ่งทำงานที่ Amazon เขียนว่า: “เราใช้ TLA+ กับโปรเจ็กต์ขนาดใหญ่ XNUMX โครงการ และในทุกกรณี การใช้งานนั้นสร้างความแตกต่างอย่างมีนัยสำคัญต่อการพัฒนา เนื่องจากเราสามารถจับแมลงที่เป็นอันตรายได้ก่อนที่พวกมันจะเข้าสู่การผลิต และเพราะมันให้ข้อมูลเชิงลึกและความมั่นใจแก่เราที่เราต้องการเพื่อดำเนินการเชิงรุก การเพิ่มประสิทธิภาพโดยไม่กระทบต่อความจริงของโปรแกรม". คุณมักจะได้ยินว่าเมื่อใช้วิธีการที่เป็นทางการ เราได้รับโค้ดที่ไม่มีประสิทธิภาพ - ในทางปฏิบัติ ทุกอย่างตรงกันข้ามเลย นอกจากนี้ ยังมีการรับรู้ว่าผู้จัดการไม่สามารถมั่นใจได้ถึงความจำเป็นของวิธีการที่เป็นทางการ แม้ว่าโปรแกรมเมอร์จะเชื่อมั่นในประโยชน์ของพวกเขาก็ตาม และ Newcomb เขียนว่า: “ตอนนี้ผู้จัดการกำลังผลักดันทุกวิถีทางที่เป็นไปได้ในการเขียนข้อกำหนดใน TLA+ และกำลังจัดสรรเวลาเป็นพิเศษสำหรับสิ่งนี้”. ดังนั้นเมื่อผู้จัดการเห็นว่า TLA+ ใช้งานได้ พวกเขาก็ยอมรับมัน Chris Newcomb เขียนสิ่งนี้เมื่อประมาณหกเดือนที่แล้ว (ตุลาคม 2014) แต่ตอนนี้ เท่าที่ฉันรู้ TLA+ ถูกใช้ใน 14 โปรเจ็กต์ ไม่ใช่ 10 โปรเจ็กต์ อีกตัวอย่างหนึ่งเกี่ยวข้องกับการออกแบบ XBox 360 มีเด็กฝึกงานคนหนึ่งมาหา Charles Thacker และ เขียนข้อกำหนดสำหรับระบบหน่วยความจำ ด้วยข้อกำหนดนี้ ทำให้พบข้อบกพร่องที่อาจไม่ถูกตรวจพบ และอาจทำให้ XBox 360 ทุกเครื่องหยุดทำงานหลังจากใช้งานไปสี่ชั่วโมง วิศวกรจาก IBM ยืนยันว่าการทดสอบของพวกเขาจะตรวจไม่พบจุดบกพร่องนี้

คุณสามารถอ่านเพิ่มเติมเกี่ยวกับ TLA+ บนอินเทอร์เน็ตได้ แต่ตอนนี้เรามาพูดถึงข้อกำหนดที่ไม่เป็นทางการกันดีกว่า เราแทบไม่ต้องเขียนโปรแกรมที่คำนวณตัวหารร่วมน้อยและอื่นๆ เลย บ่อยครั้งที่เราเขียนโปรแกรมอย่างเช่นเครื่องมือ Pretty-Printer ที่ฉันเขียนสำหรับ TLA+ หลังจากการประมวลผลที่ง่ายที่สุด โค้ด TLA+ จะมีลักษณะดังนี้:

แต่ในตัวอย่างข้างต้น ผู้ใช้มักต้องการให้เครื่องหมายร่วมและเครื่องหมายเท่ากับอยู่ในแนวเดียวกัน ดังนั้นการจัดรูปแบบที่ถูกต้องจะมีลักษณะดังนี้:

ลองพิจารณาอีกตัวอย่างหนึ่ง:

ในทางกลับกัน การจัดตำแหน่งของเครื่องหมายเท่ากับ การบวก และการคูณในแหล่งที่มานั้นเป็นแบบสุ่ม ดังนั้นการประมวลผลที่ง่ายที่สุดจึงเพียงพอแล้ว โดยทั่วไป ไม่มีคำจำกัดความทางคณิตศาสตร์ที่แน่นอนของการจัดรูปแบบที่ถูกต้อง เนื่องจาก "ถูกต้อง" ในกรณีนี้หมายถึง "สิ่งที่ผู้ใช้ต้องการ" และสิ่งนี้ไม่สามารถระบุได้ทางคณิตศาสตร์

ดูเหมือนว่าถ้าเราไม่มีคำจำกัดความของความจริง ข้อกำหนดนั้นก็ไร้ประโยชน์ แต่นั่นไม่เป็นความจริง เพียงเพราะเราไม่รู้ว่าโปรแกรมควรทำอะไร ไม่ได้หมายความว่าเราไม่จำเป็นต้องคิดว่ามันควรจะทำงานอย่างไร ในทางกลับกัน เราควรใช้ความพยายามมากขึ้นกับมัน ข้อมูลจำเพาะมีความสำคัญอย่างยิ่งที่นี่ เป็นไปไม่ได้ที่จะกำหนดโปรแกรมที่เหมาะสมที่สุดสำหรับการพิมพ์แบบมีโครงสร้าง แต่ไม่ได้หมายความว่าเราไม่ควรดำเนินการใดๆ เลย และการเขียนโค้ดตามกระแสแห่งสติไม่ได้เป็นเช่นนั้น ฉันลงเอยด้วยการเขียนข้อกำหนดหกกฎพร้อมคำจำกัดความ ในรูปแบบของความคิดเห็น ในไฟล์ Java นี่คือตัวอย่างกฎข้อใดข้อหนึ่ง: a left-comment token is LeftComment aligned with its covering token. กฎนี้เขียนด้วยภาษาอังกฤษเชิงคณิตศาสตร์: LeftComment aligned, left-comment и covering token — คำศัพท์ที่มีคำจำกัดความ นี่คือวิธีที่นักคณิตศาสตร์อธิบายคณิตศาสตร์: พวกเขาเขียนคำจำกัดความของคำศัพท์และสร้างกฎบนพื้นฐานของพวกเขา ประโยชน์ของข้อกำหนดนี้คือกฎ 850 ข้อสามารถเข้าใจและแก้ไขจุดบกพร่องได้ง่ายกว่าโค้ด 850 บรรทัด ฉันต้องบอกว่าการเขียนกฎเหล่านี้ไม่ใช่เรื่องง่าย ต้องใช้เวลาค่อนข้างมากในการแก้ไขข้อบกพร่องเหล่านั้น ฉันเขียนโค้ดเพื่อจุดประสงค์นี้โดยเฉพาะโดยบอกฉันว่ามีการใช้กฎใด เนื่องจากฉันทดสอบกฎทั้ง XNUMX ข้อนี้ด้วยตัวอย่างเล็กๆ น้อยๆ ฉันจึงไม่จำเป็นต้องแก้ไขโค้ด XNUMX บรรทัด และข้อบกพร่องนั้นค่อนข้างหาได้ง่าย Java มีเครื่องมือที่ยอดเยี่ยมสำหรับสิ่งนี้ ถ้าฉันเพิ่งเขียนโค้ด มันคงใช้เวลานานกว่ามากและการจัดรูปแบบก็จะมีคุณภาพแย่ลง

เหตุใดจึงไม่สามารถใช้ข้อกำหนดอย่างเป็นทางการได้ ประการหนึ่ง การดำเนินการที่ถูกต้องไม่สำคัญเกินไปที่นี่ การพิมพ์ที่มีโครงสร้างอาจทำให้บางคนไม่พอใจ ดังนั้นฉันจึงไม่จำเป็นต้องทำให้มันทำงานได้อย่างถูกต้องในทุกสถานการณ์ที่ไม่ปกติ ที่สำคัญกว่านั้นคือความจริงที่ว่าฉันไม่มีเครื่องมือเพียงพอ ตัวตรวจสอบโมเดล TLA+ ไม่มีประโยชน์ที่นี่ ดังนั้นฉันจะต้องเขียนตัวอย่างด้วยมือ

ข้อมูลจำเพาะที่ให้มามีคุณสมบัติเหมือนกันกับข้อกำหนดทั้งหมด มันเป็นระดับที่สูงกว่ารหัส สามารถนำไปใช้ในภาษาใดก็ได้ ไม่มีเครื่องมือหรือวิธีการในการเขียน ไม่มีหลักสูตรการเขียนโปรแกรมใดที่จะช่วยให้คุณเขียนข้อกำหนดนี้ได้ และไม่มีเครื่องมือใดที่อาจทำให้ข้อกำหนดนี้ไม่จำเป็น เว้นแต่ว่าคุณกำลังเขียนภาษาสำหรับการเขียนโปรแกรมสิ่งพิมพ์ที่มีโครงสร้างใน TLA+ โดยเฉพาะ สุดท้ายนี้ ข้อกำหนดนี้ไม่ได้บอกอะไรเกี่ยวกับวิธีที่เราจะเขียนโค้ดอย่างแน่นอน แต่เพียงระบุว่าโค้ดทำอะไรเท่านั้น เราเขียนข้อกำหนดเพื่อช่วยให้เราคิดผ่านปัญหาก่อนที่จะเริ่มคิดเกี่ยวกับโค้ด

แต่สเปคนี้ยังมีคุณสมบัติที่แตกต่างจากสเปคอื่นๆ 95% ของข้อกำหนดอื่นๆ สั้นกว่าและง่ายกว่ามาก:

นอกจากนี้ข้อกำหนดนี้เป็นชุดของกฎเกณฑ์ ซึ่งมักเป็นสัญญาณของข้อกำหนดที่ไม่ดี การทำความเข้าใจผลที่ตามมาของกฎชุดหนึ่งนั้นค่อนข้างยาก ซึ่งเป็นสาเหตุที่ฉันต้องใช้เวลามากในการแก้ไขข้อบกพร่องเหล่านั้น อย่างไรก็ตาม ในกรณีนี้ ฉันไม่สามารถหาวิธีที่ดีกว่านี้ได้

สมควรพูดสักสองสามคำเกี่ยวกับโปรแกรมที่ทำงานอย่างต่อเนื่อง โดยทั่วไปแล้วจะทำงานแบบขนาน เช่น ระบบปฏิบัติการหรือระบบแบบกระจาย มีน้อยคนนักที่จะเข้าใจสิ่งเหล่านั้นทั้งในใจหรือบนกระดาษ และฉันก็ไม่ใช่หนึ่งในนั้น แม้ว่าฉันจะทำได้ครั้งหนึ่งก็ตาม ดังนั้นเราจึงต้องการเครื่องมือที่จะตรวจสอบงานของเรา เช่น TLA+ หรือ PlusCal

เหตุใดฉันจึงต้องเขียนข้อกำหนดหากฉันรู้แล้วว่าโค้ดควรทำอย่างไร อันที่จริงฉันแค่คิดว่าฉันรู้เท่านั้น นอกจากนี้ ด้วยข้อกำหนดที่กำหนดไว้ บุคคลภายนอกไม่จำเป็นต้องดูโค้ดอีกต่อไปเพื่อทำความเข้าใจว่ามันทำอะไรกันแน่ ฉันมีกฎ: ไม่ควรมีกฎทั่วไป แน่นอนว่ามีข้อยกเว้นสำหรับกฎข้อนี้ นี่เป็นกฎทั่วไปข้อเดียวที่ฉันปฏิบัติตาม: ข้อกำหนดว่าโค้ดทำอะไรได้บ้างควรบอกทุกสิ่งที่พวกเขาจำเป็นต้องรู้เมื่อใช้โค้ดนั้น

แล้วโปรแกรมเมอร์จำเป็นต้องรู้อะไรบ้างเกี่ยวกับการคิด? ประการแรก เช่นเดียวกับทุกคน: ถ้าคุณไม่เขียน ดูเหมือนว่าคุณกำลังคิดอยู่เท่านั้น นอกจากนี้คุณต้องคิดก่อนที่จะเขียนโค้ด ซึ่งหมายความว่าคุณต้องเขียนก่อนที่จะเขียนโค้ด ข้อกำหนดคือสิ่งที่เราเขียนก่อนที่จะเริ่มเขียนโค้ด จำเป็นต้องมีข้อกำหนดสำหรับโค้ดใดๆ ที่ใครๆ ก็สามารถใช้ได้หรือเปลี่ยนแปลงได้ และ "ใครบางคน" คนนี้อาจกลายเป็นผู้เขียนโค้ดหนึ่งเดือนหลังจากเขียน ข้อกำหนดจำเพาะเป็นสิ่งจำเป็นสำหรับโปรแกรมและระบบขนาดใหญ่ สำหรับคลาส วิธีการ และบางครั้งแม้แต่สำหรับส่วนที่ซับซ้อนของวิธีการเดียวด้วยซ้ำ คุณควรเขียนอะไรเกี่ยวกับโค้ดกันแน่? คุณต้องอธิบายว่ามันทำอะไร ซึ่งก็คือสิ่งที่มีประโยชน์สำหรับทุกคนที่ใช้โค้ดนี้ บางครั้งอาจจำเป็นต้องระบุว่าโค้ดบรรลุเป้าหมายได้อย่างไร ถ้าเราผ่านวิธีนี้ในหลักสูตรอัลกอริธึม เราจะเรียกมันว่าอัลกอริธึม หากเป็นสิ่งที่พิเศษและใหม่กว่านี้ เราก็เรียกมันว่าการออกแบบระดับสูง ไม่มีความแตกต่างอย่างเป็นทางการ: ทั้งคู่เป็นโมเดลนามธรรมของโปรแกรม

คุณควรเขียนข้อกำหนดโค้ดอย่างไร? สิ่งสำคัญ: ควรสูงกว่าโค้ดหนึ่งระดับ จะต้องอธิบายสถานะและพฤติกรรม ควรเข้มงวดเท่าที่งานต้องการ หากคุณกำลังเขียนข้อกำหนดเกี่ยวกับวิธีการใช้งาน คุณสามารถเขียนเป็นรหัสเทียมหรือใช้ PlusCal ได้ คุณต้องเรียนรู้การเขียนข้อกำหนดโดยใช้ข้อกำหนดที่เป็นทางการ สิ่งนี้จะทำให้คุณมีทักษะที่จำเป็นซึ่งจะช่วยในเรื่องที่ไม่เป็นทางการด้วย คุณจะเรียนรู้การเขียนข้อกำหนดอย่างเป็นทางการได้อย่างไร? เมื่อเราเรียนรู้ที่จะเขียนโปรแกรม เราก็เขียนโปรแกรมแล้วทำการดีบั๊กมัน สิ่งเดียวกันที่นี่: คุณต้องเขียนข้อกำหนด ตรวจสอบกับตัวตรวจสอบโมเดล และแก้ไขข้อผิดพลาด TLA+ อาจไม่ใช่ภาษาที่ดีที่สุดสำหรับข้อกำหนดที่เป็นทางการ และภาษาอื่นน่าจะเหมาะกับความต้องการเฉพาะของคุณมากกว่า สิ่งที่ยอดเยี่ยมเกี่ยวกับ TLA+ คือมันทำหน้าที่สอนการคิดทางคณิตศาสตร์ได้อย่างดีเยี่ยม

จะเชื่อมโยงข้อมูลจำเพาะและรหัสได้อย่างไร? การใช้ความคิดเห็นที่เชื่อมโยงแนวคิดทางคณิตศาสตร์และการนำไปปฏิบัติ หากคุณทำงานกับกราฟในระดับโปรแกรมคุณจะมีอาร์เรย์ของโหนดและอาร์เรย์ของลิงก์ ดังนั้นคุณต้องเขียนว่ากราฟถูกนำไปใช้อย่างไรโดยโครงสร้างการเขียนโปรแกรมเหล่านี้

ควรสังเกตว่าไม่มีข้อใดข้างต้นใช้กับกระบวนการเขียนโค้ดเอง เมื่อคุณเขียนโค้ด นั่นคือ ดำเนินการขั้นตอนที่สาม คุณจะต้องคิดและคิดทบทวนโปรแกรมด้วย หากงานย่อยมีความซับซ้อนหรือไม่ชัดเจน คุณจำเป็นต้องเขียนข้อกำหนดสำหรับงานนั้น แต่ฉันไม่ได้พูดถึงโค้ดที่นี่ คุณสามารถใช้ภาษาการเขียนโปรแกรม วิธีการใดก็ได้ ซึ่งไม่เกี่ยวกับภาษาเหล่านั้น นอกจากนี้ ไม่มีข้อใดข้างต้นที่ช่วยขจัดความจำเป็นในการทดสอบและแก้ไขโค้ดของคุณ แม้ว่าโมเดลนามธรรมจะเขียนอย่างถูกต้อง แต่อาจมีข้อบกพร่องในการใช้งาน

ข้อกำหนดการเขียนเป็นขั้นตอนเพิ่มเติมในกระบวนการเขียนโค้ด ด้วยเหตุนี้จึงสามารถตรวจจับข้อผิดพลาดจำนวนมากได้โดยใช้ความพยายามน้อยลง - เรารู้สิ่งนี้จากประสบการณ์ของโปรแกรมเมอร์จาก Amazon ด้วยข้อกำหนดทางเทคนิค คุณภาพของโปรแกรมก็จะสูงขึ้น แล้วทำไมเราถึงไปโดยไม่มีพวกเขาบ่อยนัก? เพราะการเขียนเป็นเรื่องยาก แต่การเขียนเป็นเรื่องยากเพราะด้วยเหตุนี้คุณต้องคิดและการคิดก็ยากเช่นกัน การทำเป็นว่าคุณกำลังคิดนั้นง่ายกว่าเสมอ ที่นี่คุณสามารถเปรียบเทียบการวิ่งได้ - ยิ่งวิ่งน้อยเท่าไหร่ก็ยิ่งวิ่งช้าลงเท่านั้น คุณต้องฝึกกล้ามเนื้อและฝึกเขียน มันต้องใช้เวลาฝึกฝน

ข้อมูลจำเพาะอาจไม่ถูกต้อง คุณอาจทำผิดพลาดที่ไหนสักแห่ง หรือข้อกำหนดอาจมีการเปลี่ยนแปลง หรืออาจจำเป็นต้องปรับปรุง รหัสใดๆ ที่ใครใช้ก็ต้องเปลี่ยน ไม่ช้าก็เร็ว สเปคจะไม่ตรงกับโปรแกรมอีกต่อไป ตามหลักการแล้ว ในกรณีนี้ คุณต้องเขียนข้อกำหนดใหม่และเขียนโค้ดใหม่ทั้งหมด เรารู้ดีว่าไม่มีใครทำเช่นนี้ ในทางปฏิบัติ เราจะแก้ไขโค้ดและอาจอัปเดตข้อกำหนด หากสิ่งนี้จะเกิดขึ้นไม่ช้าก็เร็ว ทำไมต้องเขียนข้อกำหนดเลย? ประการแรก สำหรับผู้ที่จะแก้ไขโค้ดของคุณ ทุกคำพิเศษในข้อกำหนดจะมีมูลค่าดั่งทองคำ และบุคคลนี้อาจเป็นคุณ ฉันมักจะตำหนิตัวเองที่ไม่เฉพาะเจาะจงเพียงพอเมื่อแก้ไขโค้ด และฉันเขียนข้อกำหนดมากกว่าโค้ด ดังนั้นเมื่อคุณแก้ไขโค้ด จำเป็นต้องอัปเดตข้อกำหนดอยู่เสมอ ประการที่สอง เมื่อแก้ไขแต่ละครั้ง โค้ดจะแย่ลง ทำให้อ่านและบำรุงรักษาได้ยากขึ้น นี่คือการเพิ่มขึ้นของเอนโทรปี แต่ถ้าคุณไม่เริ่มต้นด้วยข้อกำหนด ทุกบรรทัดที่คุณเขียนจะถูกแก้ไข และโค้ดจะใหญ่และอ่านยากตั้งแต่เริ่มต้น

ตามที่กล่าวไว้ ไอเซนฮาวร์, ไม่มีการรบใดชนะตามแผน และไม่มีการต่อสู้ใดชนะโดยไม่มีแผน. และเขารู้บางอย่างเกี่ยวกับการต่อสู้ มีความเห็นว่าการเขียนข้อกำหนดเป็นการเสียเวลา บางครั้งมันก็จริง และงานก็เรียบง่ายจนไม่มีประโยชน์ที่จะคิดให้ละเอียด แต่คุณควรจำไว้เสมอว่าเมื่อคุณได้รับคำแนะนำว่าอย่าเขียนข้อกำหนด นั่นหมายความว่าคุณไม่ควรจะคิด และคุณควรคิดถึงเรื่องนี้ทุกครั้ง การคิดทบทวนงานไม่ได้รับประกันว่าคุณจะไม่ทำผิดพลาด ดังที่เราทราบ ไม่มีใครประดิษฐ์ไม้กายสิทธิ์ขึ้นมา และการเขียนโปรแกรมเป็นงานที่ยาก แต่ถ้าคุณไม่คิดทบทวนงาน คุณรับประกันได้ว่าจะทำผิดพลาด

คุณสามารถอ่านเพิ่มเติมเกี่ยวกับ TLA+ และ PlusCal ได้บนเว็บไซต์พิเศษ โดยไปที่หน้าแรกของฉันได้ ลิงค์. นั่นคือทั้งหมดสำหรับฉัน ขอบคุณสำหรับความสนใจของคุณ

โปรดจำไว้ว่านี่คือการแปล เมื่อคุณเขียนความคิดเห็น โปรดจำไว้ว่าผู้เขียนจะไม่อ่านความคิดเห็นเหล่านั้น หากคุณต้องการพูดคุยกับผู้เขียนจริงๆ เขาจะเข้าร่วมการประชุม Hydra 2019 ซึ่งจะจัดขึ้นในวันที่ 11-12 กรกฎาคม 2019 ที่เมืองเซนต์ปีเตอร์สเบิร์ก สามารถซื้อตั๋วได้ บนเว็บไซต์อย่างเป็นทางการ.

ที่มา: will.com