# HG changeset patch # User Yasutaka Higa # Date 1418193231 -32400 # Node ID 2ab39686323ad018c8f93b83c47d853f4ad89e89 # Parent 7ec73a287b63c87e3f8d2ff0261e02aa7398db32 Writing position paper .... diff -r 7ec73a287b63 -r 2ab39686323a sigse.pdf Binary file sigse.pdf has changed diff -r 7ec73a287b63 -r 2ab39686323a sigse.tex --- a/sigse.tex Wed Dec 10 15:17:57 2014 +0900 +++ b/sigse.tex Wed Dec 10 15:33:51 2014 +0900 @@ -56,14 +56,18 @@ % 本文はここから始まる \section{はじめに} 形式手法によるチェックはプログラム実装言語の処理系とユーザ間で対話的に行なわれるべきだと考える． -特に，実装言語で記述されたプログラムから仕様との対応を処理系が判断すべきだと考える． -なぜなら，仕様の定義に関わらず実行してはいけない処理などが存在するからである． +任意のプログラムに対して形式的手法が適用可能であり，必要ならばユーザが制約をさらに厳しくする． +制約の追加が対話的入力であり，反例の指摘などが対話的出力に相当する． +対話的チェックを実現するには，実装言語が通常の処理系に加えて形式的手法をサポートする必要があると考える． + +\section{形式的手法をサポートした言語} +任意のプログラムに対して形式的手法を適用可能な処理系は作成できると考える． +なぜなら，アプリケーションの仕様に関わらず実行してはいけない処理などが存在するからである． 例えば，0による除算や配列外へのアクセスはどのようなプログラムにおいても実行してはいけない． -全てのプログラムに対して共通に持つべき仕様として定義し，処理系が自動でチェックするべきである． -そうすることにより，仕様が全く記述されていないプログラムにおいても仕様をチェックすることができる． - -仕様は処理系におけるユーザ定義の満たすべき条件として定義する． +よって，全てのプログラムが共通に持つべき仕様として定義可能である． +処理系が仕様のチェック機構を持つことにより，全てのプログラムに対して形式的手法が導入可能となる． +仕様はユーザ定義の満たすべき条件として定義する． 基本的な満たすべき条件の拡張として記述することにより，仕様が存在するプログラムにも対応することができる． ここで，プログラム実装言語が自動で仕様をチェックするために必要な情報を考えたい． @@ -73,10 +77,8 @@ \section{型と証明支援系言語} 現在，私がプログラムに追加する情報として注目しているのが型である． - 型と論理は対応しており，証明が存在する定理は型によって表現できる． 満たすべき性質を証明として型が記述できれば，その型は性質を満たすと言える． - 仕様を全て論理で記述し，対応する型を記述すると仕様を満たすプログラムが記述できると思われる． しかし，論理を満たす型の記述には非常に大きなコストがかかる．