タグ

Alloyに関するyoshihiro503のブックマーク (4)

  • はてなブログ | 無料ブログを作成しよう

    うめぇヨーグルトソースでもいかがですか。個人差にもよりますが。もしよろしければ。 お久しぶりです。 最近うんめぇ〜と思ってるヨーグルトソースがあるので、書いていこうと思います。 ヨーグルトとハーブ類をもりもり使うので、そういうのがべられない方にはうんめぇソースではないです。ごめんなさい…。もしよろしければお茶だけも…旦~ 【用意する…

    はてなブログ | 無料ブログを作成しよう
  • Alloy -

    入手方法 The Alloy Analyzer - http://alloy.mit.edu/ 機能 モデル解析ツール。 一階述語論理を元にした独自のモデル記述言語によりシステムの仕様を記述することで、その仕様に矛盾や漏れがないか、制約を満たさないような反例はあるか、などを分析・検査することができる。 基構文 モジュール ファイルの先頭で指定する。 module ファイルパス/モジュール名 モジュールの定義 open ファイルパス/モジュール名 モジュールの参照 シグネチャ(型) Alloyのモデルは述語論理で表現される 論理式中の変数は必ずシグネチャ(signature)を持ち、sigキーワードにより定義される sig Person{} Person(人間)という型を定義 シグネチャはオブジェクト指向言語と同じように、継承することで差分的に定義できる。 sig Man, Woman e

  • チュートリアル - Alloy Analyzer で形式仕様記述

    ここでは、Alloy で形式的に仕様を記述/検査する方法を簡単なものから段階的に説明していきます。 ボタンの仕様を書いてみよう 集合を使って仕様を書いてみよう 以降準備中

    チュートリアル - Alloy Analyzer で形式仕様記述
  • Alloy Analyzer で形式仕様記述

    仕様を形式的に記述/検査することのできる言語やツールは、VDM, B, Z, Isabelle など他にも色々ありますが、 Alloy はそれらにくらべてより軽いフットワークで記述/検査することができるツールです。 それらのツールと Alloy との比較も、機会があればご紹介したいと思います。 2. Alloy を使った形式仕様記述の特徴 数理論理学+集合論をベースとした Alloy の言語で仕様を記述します。 書いた仕様を、簡単に検査することができます。 難しい論理式の証明などは必要ありません。 検査結果は図で表示してくれるので、結果を目視で直感的に理解することができます。 仕様で書いた振る舞いをシミュレーションすることができます。 3. このページのスコープ ここでは仕様のうち、概要レベルの仕様や、重要な部分だけを抜き出した仕様といった、抽象度の高い仕様をスコープとしています。 抽象度

    Alloy Analyzer で形式仕様記述
  • 1