y-taka-23

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

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

安全性-活性分解定理

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

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

hatsugai

theory subseq imports "~~/src/HOL/Hoare/Hoare_Logic" begin

definition is_subseq :: "'a list => 'a list => bool" where
  "is_subseq xs ys ==
    (\<exists>c.
      (\<forall>i. i + 1 < length ys --> c i < c (i + 1))
    \<and> (length ys > 0 \<longrightarrow> c (length ys - 1) < length xs)
    \<and> (\<forall>i. i < length ys \<longrightarrow> ys ! i = xs ! (c i)))"

fun is_subseq2 :: "'a list => 'a list => bool" where

shinyquagsire23

DeviceInfo(softwareRevision, isOn, 
SceneLightState(color, powerOnBehavior, deviceInfo
Light(id,
Capabilities(dimmable, customState
PowerOnBehavior(option

hueplay, huebloom, hueiris, huelightstrip, huego, plug, bollard, wallspot, groundspot, flexiblelamp, wallshade, walllantern

[ea:44:13:bd:db:59]  Service [b8843add-0000-4aa1-8794-c3f462030bda]              Unknown, ble_firmware_update?
[ea:44:13:bd:db:59]    Characteristic [b8843add-0004-4aa1-8794-c3f462030bda]

norio-nomura

$ echo 'import Dispatch; func f() {}; DispatchQueue.global(qos: .default).async { f() }; dispatchMain()'|swiftc -
$ lldb
(lldb) target create main
Current executable set to 'main' (x86_64).
(lldb) b f
Breakpoint 1: 9 locations.
(lldb) process launch -v DYLD_LIBRARY_PATH=/usr/lib/system/introspection -v DYLD_INSERT_LIBRARIES=/Applications/Xcode.app/Contents/Developer/usr/lib/libBacktraceRecording.dylib
Process 33297 launched: '/Users/norio/github/swift-dev/SourceKitten/main' (x86_64)
Process 33297 stopped
* thread #2, queue = 'com.apple.root.default-qos', stop reason = breakpoint 1.1

omochi

func c(_ g: @escaping (Int) -> Void) {}

func a() {
    let f: ((Int) -> Void) -> Void
    
    f = { (g) -> Void in
        c(g)
    }
}

omochi

// swift/stdlib/public/runtime/Metadata.cpp をプリプロセッサのみ実行した結果から抜粋

struct ValueWitnessTable;

namespace value_witness_types {
  typedef OpaqueValue * (*initializeBufferWithCopyOfBuffer) (ValueBuffer *, ValueBuffer *, const Metadata *);
  typedef void (*destroy) (OpaqueValue *, const Metadata *);
  typedef OpaqueValue * (*initializeWithCopy) (OpaqueValue *, OpaqueValue *, const Metadata *);
  typedef OpaqueValue * (*assignWithCopy) (OpaqueValue *, OpaqueValue *, const Metadata *);
  typedef OpaqueValue * (*initializeWithTake) (OpaqueValue *, OpaqueValue *, const Metadata *);

NobukazuHanada

class Number {}
class Zero : Number {}
class Succ<N:Number> : Number {}

typealias One = Succ<Zero>
typealias Two = Succ<Succ<Zero>>
typealias Three = Succ<Succ<Succ<Zero>>>

class Eq<S: Number, T: Number> {}
class Add<S: Number, T:Number> : Number {}

tk0miya

(For English readers: please read https://github.com/sponsors/tk0miya instead)

@tk0miya の企業・個人スポンサーを募集します

@tkomiya は、日本在住の OSS 開発者です。
趣味として Sphinx や pycmark、 blockdiag などの OSS の開発やメンテナンスに携わっています。

ここ数年の活動の中心は Sphinx です。 Sphinx は Python や Linux カーネルをはじめとして、数多くの OSS のドキュメントに利用されているドキュメンテーションツールです。 Sphinx プロジェクトはごく少人数のメンテナによって活動しており、(明確な役割として定義はされていないものの) リードメンテナ、メインメンテナとして活動しています。

tanishiking

シンボリック実行入門メモ

参考文献

• Symbolic execution - Wikipedia
• King, James C. "Symbolic execution and program testing." 1976 (pdf)
• DART: Directed Automated Random Testing
• CUTE: A Concolic Unit Testing Engine for C
• Jeff Foster, "Symbolic Execution," 2011 (pdf)
• シンボリック実行に入門しようとした - 一生あとで読んでろ
• テスト入力値の自動生成と、concolic testing - ソフトウェアの品質を学びまくる

pocke

class Binding
  def return_if(name)
    eval "return #{name}" if local_variable_get(name)
  end
end
def foo(v)
  binding.return_if(:v)
  'v is nil'
end