{"text_format":"2","workbook":"xls","n_sheets":1,"sheets":["report2"],"not_rendered":{"charts":0,"images":0,"macros":0,"external_links":1,"defined_names":2,"comments":0,"pivot_tables":0},"unopened":[],"bounds":{"document_bytes":16777216,"sheet_cells":100000,"run_cost":"one","rows_first":2000,"rows_last":500,"rows_between":2000,"halvings":0,"cell_chars":16384,"cell_head_chars":4096},"cells_cut":0,"cells_raw":0,"read":"whole","date_system":"1900","formulas":"cached_only"}

{"sheet":"report2","index":0,"n_rows":30,"n_cols":5,"rows_kept":30,"cut":false,"hidden":false,"merged":[[0,2,0,3],[0,4,0,5],[1,2,1,3],[1,4,1,5],[2,2,2,3],[2,4,2,5],[3,2,3,3],[4,2,4,3],[5,2,5,3],[6,2,6,3],[7,2,7,3],[8,2,8,3],[9,2,9,3],[11,2,11,3],[11,4,11,5],[12,2,12,3],[12,4,12,5],[13,2,13,3],[15,2,15,3],[16,2,16,3],[17,2,17,3],[19,2,19,3],[21,2,21,3],[22,2,22,3],[28,2,28,3]],"flags":["formulas_cached_only"]}
[null,"1.","Record Nr.",null,"UNINA990006781830403321"]
[null,null,"Autore",null,"Beecher, Jonathan"]
[null,null,"Titolo",null,"Charles Fourier : the visionary and his world / Jonathan Beecher"]
[null,null,"Pubbl/distr/stampa",null,"Berkeley : University of California Press, c 1986"]
[null,null,"Descrizione fisica",null,"XVIII, 602 p. tav. f.t. 23 cm"]
[null,null,"Disciplina",null,"335.2"]
[null,null,"Locazione",null,"FSPBC"]
[null,null,"Collocazione",null,"XII A 1135"]
[null,null,"Lingua di pubblicazione",null,"Italiano"]
[null,null,"Formato",null,"Materiale a stampa"]
[null,null,null,"Livello bibliografico","Monografia"]
[null,"2.","Record Nr.",null,"UNINA9910148969103321"]
[null,null,"Titolo",null,"形式手法入門 :  ロジックによるソフトウェア設計 / /  中島震著"]
[null,null,"Pubbl/distr/stampa",null,"東京, : オーム社, 2012.4"]
[{"$nulls":4},"東京 : , : オーム社, , 2012"]
[null,null,"ISBN",null,"4-274-83011-X"]
[null,null,"Descrizione fisica",null,"オンライン資料1件"]
[null,null,"Classificazione",null,"007.63"]
[{"$nulls":4},"007.61"]
[null,null,"Soggetti",null,"ソフトウェア工学"]
[{"$nulls":4},"システム設計"]
[null,null,"Lingua di pubblicazione",null,"Giapponese"]
[null,null,"Formato",null,"Materiale a stampa"]
[null,null,null,"Livello bibliografico","Monografia"]
[null,null,null,"Note generali","電子資料の出版情報: KinoDen, 2018"]
[{"$nulls":4},"電子資料の出版情報: ProQuest, 2018"]
[{"$nulls":4},"参考文献: p[203]-210"]
[{"$nulls":4},"索引: p[211]-216"]
[null,null,"Nota di contenuto",null,"表紙 -- まえがき -- 目次 -- 1章　論理で考える -- 1.1　形式手法の概要 -- 1.1.1　高信頼化の総合技術 -- 1.1.2　複雑さと抽象化 -- 1.1.3　工学的な道具 -- 1.2　発展の経緯 -- 1.2.1　形式手法の変遷 -- 1.2.2　設計法と形式手法 -- 1.2.3　形式仕様言語の分類 -- 2章　指先で考える -- 2.1　Alloy入門 -- 2.1.1　Alloyの面白さ -- 2.1.2　Compositeパターン -- 2.1.3　抽象データの表現と解析 -- 2.1.4　機能仕様の表現と解析 -- 2.2　Alloyの基礎 -- 2.2.1　関係論理の考え方 -- 2.2.2　解析の方法 -- 2.2.3　有界モデル発見の限界 -- 2.3　Alloyとその周り -- 2.3.1　Alloyの歴史 -- 2.3.2　SATとSMT -- 3章　機能仕様を論理で考える -- 3.1　手続きとデータ構造 -- 3.1.1　状態ベースの仕様 -- 3.1.2　例題による形式手法の比較 -- 3.1.3　形式手法の比較 -- 3.1.4　2つの解釈 -- 3.2　正しさの基準 -- 3.2.1　正しさのいろいろ -- 3.2.2　型と型検査 -- 3.2.3　状態ベース仕様の証明条件 -- 4章　リファインメントを検査する -- 4.1　リファインメントとは -- 4.1.1　要求仕様とリファインメント -- 4.1.2　段階的な詳細化 -- 4.1.3　段階的な機能追加 -- 4.2　リファインメントの基礎 -- 4.2.1　2つの抽象レベル -- 4.2.2　模倣関係 -- 4.3　リファインメント検査 -- 4.3.1　リファインメントの証明条件 -- 4.3.2　Alloyとリファインメント -- 5章　オブジェクト指向デザインを検査する -- 5.1　クラス図とOCL -- 5.1.1　オブジェクト指向ソフトウェア開発とUML -- 5.1.2　静的な情報構造 -- 5.1.3　メソッドの機能振る舞い -- 5.2　モデリング言語OCL -- 5.2.1　OCLの変遷 -- 5.2.2　OCLの特徴 -- 5.2.3　3値論理 -- 5.3　オブジェクト指向概念と形式手法 -- 5.3.1　オブジェクト指向形式仕様言語 -- 5.3.2　オブジェクト指向デザインの形式化 -- 6章　振る舞い仕様を検査する -- 6.1　状態遷移システム -- 6.1.1　状態遷移マシン -- 6.1.2　述語論理による解釈 -- 6.1.3　UMLステート図 -- 6.2　"]
[{"$nulls":4},"時相的な振る舞いの自動解析 -- 6.2.1　時相論理 -- 6.2.2　有界モデル検査 -- 6.2.3　LTLの有界モデル検査 -- 6.2.4　ロジック・モデル検査 -- 6.2.5　イベント駆動スタイル -- 7章　プログラム検査を論理で考える -- 7.1　プログラムの意味 -- 7.1.1　Floyd/Hoareの方法 -- 7.1.2　プログラムの振る舞い解析の例 -- 7.1.3　VDMへの影響 -- 7.2　プログラムの検証 -- 7.2.1　ソフトウェア・モデル検査 -- 7.2.2　コントラクト -- 7.3　テストケースの自動生成 -- 7.3.1　ソフトウェアのテスト技術 -- 7.3.2　仕様に基づくテストケース自動生成 -- 7.3.3　モデル検査の利用 -- 付録　モデル規範形式手法の流れ -- A.1　概要 -- A.2　VDM -- A.3　Z記法とBメソッド -- A.4　集合ベースの方法 -- 索引 -- 奥付."]