Model Base内検索 / 「「形式手法の独学」のPFD」で検索した結果

• 「形式手法の独学」のPFD
  ... 「形式手法の独学」のPFD 各プロセスの説明 P001_命題論理を学習する P002_述語論理を学習する P003_集合論_関係_順序を学習する P100_状態遷移システムの構成概念を理解する P021_モデル発見器を学習する P200_仕様の推敲を練習する P004_時相論理を学習する P031_モデル検査器を学習する P300_設計の検証を練習する P900_知見を整理する 各成果物の説明 I001_事例や業務経験 I002_数理論理学の教本 I003_離散数学の教本 I004_様相論理を含む数理論理学の教本 I005_モデル発見器_Alloy I006_Alloyのチュートリアル I007_モデル検査...
• 形式手法の独学
  ...う。 「形式手法の独学」のPFD PFD Process Flow Diagram について PFDはコンサルタントの清水吉男先生から2005年に教えていただいた図式で、 チュートリアルも公開されている。PFDはソフトウェアの開発段取を 可視化すること(自分は"作業段取の設計"と言っている)に利用できる。 PFDについて詳しくは、以下のURL参照してほしい。 http //homepage3.nifty.com/koha_hp/process/Proc.Index.html PFDを一言で説明すると、「成果物とプロセスの連鎖を表現する図式」ということになる。 ここで言う成果物とは必ずしも文書やソースコードといった有形な ものに限らず、経験、知識、判断といった類の無形の成果もその範疇に入る。 成果物は矩形で図示さ...
• トップページ
  ...う。 「形式手法の独学」のPFD PFD Process Flow Diagram について PFDはコンサルタントの清水吉男先生から2005年に教えていただいた図式で、 チュートリアルも公開されている。PFDはソフトウェアの開発段取を 可視化すること(自分は"作業段取の設計"と言っている)に利用できる。 PFDについて詳しくは、以下のURL参照してほしい。 http //homepage3.nifty.com/koha_hp/process/Proc.Index.html PFDを一言で説明すると、「成果物とプロセスの連鎖を表現する図式」ということになる。 ここで言う成果物とは必ずしも文書やソースコードといった有形な ものに限らず、経験、知識、判断といった類の無形の成果もその範疇に入る。 成果物は矩形で図示さ...
• 「状態遷移システムの構成概念を理解する」のPFD
  更新日2013-01-31 [ 形式手法の独学 ] / [ 「形式手法の独学」のPFD ] 「状態遷移システムの構成概念を理解する」のPFD 各プロセスの説明 P101_FSMの数学モデルを学ぶ P102_状態遷移に関わる用語の意味を考える P103_UMLでの"状態"という用語の運用について考える P104_状態遷移の合成ついて考える P105_状態遷移時のアクションについて考える P106_ProtocolStateMachine図とBehavioralStateMachine図の作図目的の違いを考える P107_ステートマシンの作図を練習する 各成果物の説明 I101_FSMの数学モデルの定義 I102_UMLのチュートリアル I103_状態...
• 「仕様の推敲を練習する」のPFD
  更新日2013-01-31 [ 形式手法の独学 ] / [ 「形式手法の独学」のPFD ] 「仕様の推敲を練習する」のPFD 各プロセスの説明 P201_練習用の仕様情報を作成する P201'_仕様を推敲する P202_仕様情報を数学的な構造に翻訳する P202'_仕様を表す構造を修正する P203_着目する性質を考察する P204_着目する性質を述語化する P205_充足例を探索する P205'_反例を探索する P206_充足例のインスタンスを観察する P206'_反例のインスタンスを観察する P299_知見を整理する←繰り返しの練習によって得られた経験を整理する 各成果物の説明 D201_仕様情報 D...
• メニュー
  メニュー トップページ 形式手法の独学 Alloy Analyzer 更新履歴 取得中です。 ここを編集
• Alloy Analyzer
  抽象によるソフトウェア設計／付録 A 練習問題 解答例 形式仕様記述ツールAlloy Analyzerの解説本「Software Abstractions」の邦訳「抽象によるソフトウェア設計－Alloyではじめる形式手法」が出版されたので、これを機会に書籍の付録にある練習問題に(興味のある箇所をつまみ食い的に)挑戦してみる。 ⇒抽象によるソフトウェア設計／付録 A 練習問題 解答例 　 　 　 　 　 　 Today - Yesterday -
• A.1.2 関係計算・述語論理形式
  更新日 2011-09-03 [ Alloy Analyzer ] / [ 抽象によるソフトウェア設計／付録 A 練習問題 解答例 ] 本文3.5.2から察するに、"述語論理形式"とは限量子Qを含む Q x e | F の形式のことを指していると思われる。 関係rの各性質(非空的、推移的、非反射的、、、)について、 A.1.1の記述と自分で考えた述語論理形式の記述が同値になるか否かの検査記述を以下のように書いてみた。 assert ReformulateOK { all r univ- univ { -- nonempty (some r) iff (some x, y univ | x- y in r) -- transitive (r.r in r) iff (al...
• 抽象によるソフトウェア設計／付録 A 練習問題 解答例
  [ Alloy Analyzer ] A.1 論理の問題 A.1.1 二項関係の性質 (省略する) A.1.2 関係計算・述語論理形式 A.1.3 モデリング時の関係的性質 A.1.4 ナビゲーションのリファクタリング A.1.5 木を特徴付ける A.1.6 スパニング木 A.1.7 リングを特徴付ける A.1.8 無向グラフの非循環性を定義する A.1.9 推移閉包を公理化してみる A.1.10 アドレス帳の制約と式 A.1.11 地下鉄をモデリングする A.2 単純なモデルを拡張する A.2.1 電話のスイッチング接続 A.2.2 アドレス帳の不変条件を保存する A.2.3 囚人の割り当て A.3 古典的パズル ...
• A.3.1 驚くような三段論法
  更新日2011-09-03 [ Alloy Analyzer ] / [ 抽象によるソフトウェア設計／付録 A 練習問題 解答例 ] Doris Day の歌 Everybody loves my baby but my baby don’t love nobody but me. この歌をいくつかの制約で形式化し、Gries の推論をアサーションにせよ。 Doris Day の歌の主張を 述語DorisDay 、「私は私の彼だ」を 述語I_am_my_baby、Geriesの推論を示す 述語Gries は以下となる。 pred Greies{ DorisDay = I_am_my_baby } "私"や、"私の彼"、"好き"などの構造を以下のように定義すると...
• プラグイン/ニュース
  ニュース @wikiのwikiモードでは #news(興味のある単語) と入力することで、あるキーワードに関連するニュース一覧を表示することができます 詳しくはこちらをご覧ください。 ＝＞http //atwiki.jp/guide/17_174_ja.html たとえば、#news(wiki)と入力すると以下のように表示されます。 マニュアル作成に便利な「画像編集」機能を提供開始！ - ナレッジ共有・社内wikiツール「NotePM」：時事ドットコム - 時事通信 マニュアル作成に便利な「画像編集」機能を提供開始！ - ナレッジ共有・社内wikiツール「NotePM」 - PR TIMES 【アイプラ】リセマラは必要？当たりキャラランキング【IDOLY PRIDE】 - Gamerch(ゲーマチ) 篠原悠希×田中芳樹が明かす「歴史ファンタジー小説...
• A.1.11 地下鉄をモデリングする
  更新日2011-09-03 [ Alloy Analyzer ] / [ 抽象によるソフトウェア設計／付録 A 練習問題 解答例 ] ( a ) 路線line にある駅の集合がS である "路線line上の駅の集合はSである" という述語を定義する。 路線lineの各区間の始端の集合は line.univ 、各区間の終端の集合は univ.line となる。 路線lineの駅の集合は始端と終端の和集合となる。 pred stations[line univ- set univ, S set univ]{ let Points = univ.line+line.univ | S = Points } ( b ) line には切れ目がない "路線lineには切れ目がない&qu...
• @wiki全体から「「形式手法の独学」のPFD」で調べる

更新順にページ一覧表示 | 作成順にページ一覧表示 | ページ名順にページ一覧表示 | wiki内検索