y-taka-23

形式手法特論：公平性制約の位相的特徴づけ

• Kernel/VM 探検隊 @ 関西 12 回目
• SpeakerDeck

安全性-活性分解定理

並行システムにおいて、安全性（safety）と 活性 (liveness）という仕様のクラスは広く知られており、それぞれ「悪いことが決して起こらない」「良いことがいつか起こる」として説明されることが多い。この非形式的な定義に対して、1985 年、Alpern と Schneider によって、以下のような位相的な特徴づけが与えられた。

• 定義：安全性とは閉集合のことである

y-taka-23

Elm による大学入学共通テスト指南

• TL;DR: オンライン実行環境作ってるよ (WIP)
• https://github.com/y-taka-23/dncl-playground
• https://elm-jp.connpass.com/event/280401/

共通テスト手順記述標準言語 (DNCL)

y-taka-23

module signal

enum LightState { On, Off, Blink }

abstract sig Light {
  var state: one LightState
}

one sig Red, Green extends Light {}

y-taka-23

#!/bin/bash

rm -f cut.mov
rm -f palette.png
rm -f encoded.gif
rm -f output.gif

ffmpeg -ss 10 -to 15 -i input.mov -c copy cut.mov
ffmpeg -i cut.mov -vf fps=30,scale=340:-1:flags=lanczos,palettegen palette.png
ffmpeg -i cut.mov -i palette.png -filter_complex "fps=30,scale=340:-1:flags=lanczos[x];[x][1:v]paletteuse" encoded.gif

y-taka-23

module Sample where

import Language.Haskell.Liquid.Prelude ( liquidError )

{-@ safeHead :: { xs:[a] | len xs > 0 } -> a @-}
safeHead []      = liquidError "empty list"
safeHead (x : _) = x

-- badUsage = safeHead [] -- => Liquid Type Mismatch

y-taka-23

open util/ordering[Time]

sig Time {}

abstract sig Event {
    pre, post : Time,
} {
    post = pre.next
}

y-taka-23

// ************************************
//   命題論理のシークエント計算のモデル
// ************************************

// 論理式
abstract sig Formula {}

// 原子命題
sig Atom extends Formula {}

y-taka-23

// **************************************************
//  AWS セキュリティグループのモデル
// **************************************************

// 通信プロトコル
enum Protocol { TCP, UDP, ICMP }

// 通信ポート
sig Port {}

y-taka-23

Parameter A : Type.
Parameter beq_A : A -> A -> bool.

Section Uniq.

Require Import Arith List.

Hypothesis beq_A_true : forall x y : A,
                        beq_A x y = true -> x = y.
Hypothesis beq_A_false : forall x y : A,

y-taka-23

/*
 * Resource Sharing Problem (Example for Deadlock)
 */

mtype = { LOCK, UNLOCK };

proctype Client(chan to_res1, to_res2) {
    if
    ::  to_res1 ! LOCK(_pid);
        to_res2 ! LOCK(_pid);