少しづつ進んでいるが、後退しているかも。縦・横チェーンの結果の連動性?の説明が、口述的であったのをどうにか形式化 しようと試みた。合成結果R0の動作が、明らかに連動するSpecの動作にtrace containmentされること を示めせば、良いだろう(ほんとうか…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。