『構成的数学の体系と実践』
構成的数学の体系と実践
BHK解釈
以下の
命題
は許容されない
LPO(the Limited Principle of Omniscience)
WLPO(the Weak Limited Principle of Omniscience)
LLPO(the Lesser Limited Principle of Omniscience)
なんもわからん
構成的数学
Bishopの構成的数学
構成的証明
構成的帰納的数学
Bishopの体系
構成的プログラミング
形式手法
IEC 61508
SIL(safety integrated level、安全度水準)に応じた推奨する開発手法がある
SIL2〜SIL4は形式手法の対象
ISO/IEC 15408
#スライド
#形式手法
#文献