? ? ? CSSE7100/3100 Reasoning about Programs有關(guān)程序的推理

　　1.一般課程信息

　　UQ學(xué)生：請從Learn.UQ或mySI-net訪問個人資料，以訪問此個人資料中保存的所有課程參與者詳細(xì)信息。

　　1.1課程詳情

　　課程編號： CSSE7100

　　課程名稱：關(guān)于程序的推理

　　協(xié)調(diào)單位：信息技術(shù)與電氣工程學(xué)院

　　學(xué)期： 2020年第1學(xué)期

　　模式：內(nèi)部

　　級別：研究生課程

　　地點(diǎn)：圣盧西亞

　　臺數(shù)： 2

　　每周接觸時間： 3C

　　先決條件： MATH7861和CSSE7023

　　課程說明：編寫軟件的目的是要執(zhí)行所需的任務(wù)。編寫此類軟件需要算法問題解決能力;正確地做到這一點(diǎn)要求我們精確地處理手頭的任務(wù)，并能夠推斷出實(shí)現(xiàn)滿足任務(wù)的精確要求。這門編程高級課程介紹了結(jié)構(gòu)化的形式化方法，這些方法用于：指定程序的期望行為，表明程序就其規(guī)范而言是正確的，并從規(guī)范中推導(dǎo)算法。這些技術(shù)旨在幫助開發(fā)人員解決編程問題并生產(chǎn)高質(zhì)量的軟件。

　　假設(shè)背景：

　　要求學(xué)生至少完成2門編程課程，并對謂詞邏輯有扎實(shí)的理解。

　　1.2課程簡介

　　本課程的主要目的是向您介紹一些技術(shù)和工具，使您可以對程序進(jìn)行推理，以表明該程序符合所有有效輸入的規(guī)范，而不僅僅是單個測試輸入。換句話說，您將學(xué)習(xí)驗(yàn)證程序是否滿足其規(guī)范。

　　在進(jìn)入關(guān)于程序的推理時，您將學(xué)習(xí)基本的編程技術(shù)以及謂詞邏輯的證明。該課程將這兩部分學(xué)習(xí)結(jié)合在一起，以使用邏輯推理程序。您還將學(xué)習(xí)使用最先進(jìn)的工具來自動化和檢查程序正確性的證明。

　　總體而言，該課程可以看作是編程的高級課程，重點(diǎn)是提高您的能力，以確保您編寫的程序滿足其規(guī)范。

　　根據(jù)先前學(xué)生的反饋對課程進(jìn)行更改

　　“ 我認(rèn)為另一件事會很好，那就是以計(jì)算機(jī)語言實(shí)際完成的一些示例或練習(xí)，也許只是一些簡單的程序，可以從規(guī)范中提取規(guī)范并進(jìn)行驗(yàn)證，或者在從規(guī)范中派生出程序后編寫。我理解這將需要學(xué)生熟悉特定的語言，但是每個學(xué)生都應(yīng)該熟悉CSSE早期課程中的python或java，這樣做將有助于彌合理論與實(shí)際應(yīng)用之間的鴻溝。 ”

　　現(xiàn)在，該課程以Dafny編程語言為基礎(chǔ)。Dafny起源于Microsoft Research，現(xiàn)在也正在Amazon Web Services中開發(fā)。它與基于C的語言(例如C#和Java)有很多共同點(diǎn)。

　　“ 我希望本課程有更多內(nèi)容：例如，學(xué)習(xí)使用講座中提供的一些工具來展示真實(shí)程序的正確性，討論如何將正式方法應(yīng)用于生產(chǎn)軟件以及在何處應(yīng)用正式方法，自動證明等。 。 “

　　現(xiàn)在，該課程將Dafny驗(yàn)證工具廣泛用于自動和交互式推理。

　　“ 對于作業(yè)2，只有一個問題占20%的問題有點(diǎn)令人生畏-如果某人一開始就努力將諸如特定問題的說明之類的內(nèi)容放在一起，那可能會花費(fèi)很多課程費(fèi)用-這樣的話，如果價(jià)值20%的作業(yè)多于一個問題，那就更好了。 ”

　　“ 除主要問題外，第二個作業(yè)本可以有幾個較小的問題?！?/span>

　　CSSE7100/3100 Reasoning about Programs有關(guān)程序的推理該課程現(xiàn)在有4個小作業(yè)，而不是2個大作業(yè)。學(xué)生的工作量與前幾年相同，但分布更多，有更多的反饋機(jī)會。