morning_reading https://blog.hatena.ne.jp/morning_reading/ 毎朝30分読書会 https://morning-reading.hatenadiary.org/ 今日は第4章の 4.4 型と型検査からです。 Alloy における型システムは、解析前のエラー検出と、フィールドのオーバーロードを解消(同じフィールド名がどのシグネチャのものかを解決する)に用いられる シグネチャには「基本型」がつけられる A1 が A の拡張シグネチャの場合 A1 の型は A の型の部分型であると言う 部分集合シグネチャの場合そのシグネチャ自体の型はなく親の型がつけられる。親(母集団)がシグネチャの和集合の場合(sig C in A + B {})、その型は親の型の和集合となる(型の和集合! しかし「型とは値の集合」という解釈を考えるとこれは自然なことか) 式は「関係型」に属… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fmorning-reading.hatenadiary.org%2Fentry%2F20111207%2Fp1" title="抽象によるソフトウェア設計 第4章 言語 その4 - 毎朝30分読書会" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2011-12-07 00:00:00 rich https://morning-reading.hatenadiary.org/entry/20111207/p1 1.0 100%