本を読む

「抽象によるソフトウエア設計 - Alloyで始める形式手法」を読んでみる

二項関係 ([1], P220)

		run {
			 // ここを変更する
		} for 4
      

非空的

      some r : univ -> univ {
		some r
	  }
      

推移的

      some r : univ -> univ {
		r.r in r
	  }
      

非反射的

      some r : univ -> univ {
		no iden & r
	  }
      

対称的

		some r : univ -> univ {
			~r in r
		}
      

関数的

		some r : univ -> univ {
			~r.r in iden
		}
      

単射的

		some r : univ -> univ {
			r.~r in iden
		}
      

全域

		some r : univ -> univ {
			univ in r.univ
		}
      

全射的

		some r : univ -> univ {
			univ in univ.r
		}