新機能 イベント参加者限定の懇親会やミニイベント開催に対応した「サブイベント機能」をリリースしました。イベント運営を簡素化し、参加者の登録漏れや確認漏れを防ぐのにご活用ください。主催の方はサブイベントを作成するから、参加者の方はサブイベントが設定されているイベントに参加するから詳細をご確認いただけます。
広告
| 募集内容 | 一般 3000円（前払い） 先着順 |
|---|---|
| 申込者 |    |
| 開催日時 | 2024/08/04(日) 13:00 ～ 18:00 |
| 募集期間 | 2024/07/21(日) 00:00 〜 |
| 会場 | Zoom オンライン |
| 前払いについて | 前払いについての連絡先: (参加者にのみ公開されます) |
キャンセル・参加費用の払い戻しについて主催者からの説明: お申し込み後のキャンセルはできません．セミナーについての説明をよくお読みいただき，十分ご検討の上お申し込みください | |
領収データの発行: 発行しない(詳しくはこちら) | |
| 出席登録 | (イベント開始時間の2時間前から終了時間まで、参加者のみに公開されます) |
広告
イベントの説明
セミナーの内容
プログラム検証の理論に基づいて，プログラムの正しさを数学的に証明するトレーニングをするセミナーです．
プログラム検証の理論を身につけると，プログラムの仕様記述，仕様の分析，コーディング，コードレビュー，テストといったプログラミング全般においてよい効果があると考えています．
このセミナーでは定理証明器を使用しません．その理由を説明します．定理証明器のよいポイントは3つあります．1つ目は証明の正しさをチェックしてくれる点，2つ目は証明の一部を人間の代わりに実行してくれる点，最後は証明の全体を構成して管理してくれる点です．応用においてはこれらの支援がとても役に立ちます．しかしその一方で，支援が強力であることから，理論や対象の理解が不十分であったとしても証明ができてしまうという問題もあります．
定理証明器に頼らず紙とペンを使って机上で証明することになると，証明のすべての詳細を自力で行う必要があります．証明の構成を考え，戦略を立て，どこまで証明できているか，何が残っているか，何が使えるのかを管理する必要があります．定理証明器の利点である証明のチェックがないので間違いを犯す可能性は高まりますが，その分，理論の理解を深め，証明の力を向上させることができると思います．特に構成力を高めることができると思います．定理証明器の上ではできる証明が，真っ白い紙の上では構成できないことを知れば，そこに訓練すべきことがあることがわかります．
プログラム
プログラム検証の理論を段階的に解説します．各段階で解説した部分に関する証明問題をやっていただきます。答え合わせのときには、証明の解説に参加していただきます。これが短時間で力をつけるよい方法だからです。
- 最弱事前条件
- 正当性の条件
- 代入文
- 条件文
- ループ
- 関数呼び出し
※ 進捗に応じて，一部内容をスキップする場合があります．原則として，全問題を消化することよりも，確実な理解を優先します．
講師について
株式会社PRINCIPIA代表取締役 初谷 久史
プロセス代数 CSP に基づいた検査ツール SyncStitch 開発者
国立情報学研究所トップエスイープロジェクト「モデル検査特論」講師
セミナー参加の前提条件
前提知識
- プログラミングの基礎知識
- 1階述語論理
必要なもの
- 計算用紙と筆記具、またはエディタ
Zoom URL
CONNPASS のメッセージにてお知らせします。
配布物
スライド資料を CONNPASS のメッセージで配布します．申し込まれるタイミングによっては，PayPal でお使いのメールアドレスに送付する場合もあります．メールが受信できることをご確認ください．
注意事項
- 配布資料の公開は禁止です．
- Zoom 上での表示名を CONNPASS のユーザ名と合わせていただけると助かります．荒しを防止するためです．
連絡先
ご質問等がありましたら isaac@principia-m.com までお気軽にご連絡ください．
広告
資料資料をもっと見る／編集する
資料が投稿されると、最新の3件が表示されます。
広告
フィード
2024/08/04(日)
13:00 〜 18:00 募集期間
2024/07/21(日) 00:00 〜
2024/08/04(日) 12:30
広告
会場
Zoom
オンライン
管理者
hatsugai
広告
広告
エンジニアをつなぐ
connpass は株式会社ビープラウドが開発・運営しています