Skip to content

Instantly share code, notes, and snippets.

💭
I may be slow to respond.

Kuniwak Kuniwak

💭
I may be slow to respond.
Block or report user

Report or block Kuniwak

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@Kuniwak
Kuniwak / 1-playground.tla
Last active May 27, 2019
解決しました(コメント参照) ~~なぜ、Temporal properties were violated になるのかわかりません。。。~~
View 1-playground.tla
----------------------------- MODULE playground -----------------------------
VARIABLES varTable
\* Initial Predicate:
Init == varTable = { <<0, "a">>, <<1, "b">> }
\* Next-state relation:
Next == varTable' = { <<2, "c">> }
@Kuniwak
Kuniwak / Config.xcconfig
Created Feb 28, 2019
Useful xcconfig for SwiftSyntax
View Config.xcconfig
CUSTOM_SWIFT_SOURCE = $(SRCROOT)/path/to/swift-source
HEADER_SEARCH_PATHS = $(CUSTOM_SWIFT_SOURCE)/swift/include/swift-c/SyntaxParser
LIBRARY_SEARCH_PATHS = $(CUSTOM_SWIFT_SOURCE)/build/Ninja-RelWithDebInfoAssert/swift-macosx-x86_64/lib
LD_RUNPATH_SEARCH_PATHS = $(LIBRARY_SEARCH_PATHS)
View stupid_verification_approach.md

やりたいこと

GUI アプリケーションのドメインを、小さなステートマシンの協調として表現しようとすると、頻繁にバグる上に単体テストの入力空間が手書きするにはでかくて、適切なサンプルを選ぶのも作るのもだるい。そこで、コードのアノテーションから状態機械のモデルを作って性質を証明するようにできたら、結構楽になる。

疑問

このように、別言語のアノテーションで状態機械のモデルをつくるアプローチをほとんど知らないのだが、既存でそういうのあるだろうか。

超雑な例

View typescript-inferring.ts
class A { a: "a" = "a"; }
class B { b: "b" = "b"; }
interface X {
a: Y<A>;
b: Y<B>;
}
interface Y<T> { t: T; }
type Z<T> = { [key in "a"]: Y<T> };
@Kuniwak
Kuniwak / 2013_11_15_githubjp_note.markdown
Last active Oct 30, 2018
「GitHub トレーニングチームから学ぶ Git の内部構造」のノートです。 曖昧なところもあるので、間違いがあったら教えてください! http://connpass.com/event/3808/
View 2013_11_15_githubjp_note.markdown

GitHub トレーニングチームから学ぶ Git の内部構造

Graphs, Hashes, and Compression, Oh My!

Hash について

従来の CVCS (集中バージョン管理システム)のリビジョン番号は連番。 SVN はサーバーにデプロイした時点でリビジョン番号1と設定される。

View Result.swift
public enum Result<T, E> {
case success(T)
case failure(because: E)
public var isSuccess: Bool {
switch self {
case .success:
return true
case .failure:
View PrefixedArray.swift.gyb
%{
number_of_generated = 5
}%
public struct PrefixedArray<Element, RestElements> {
public let prefix: Element
public let rest: RestElements
View compile-time-hour.swift
public protocol PositiveInt: Equatable {}
public struct Succ<T>: PositiveInt where T: PositiveInt {
private let x: T
fileprivate init(_ x: T) { self.x = x }
}
public struct Zero: PositiveInt {
public static func ==(lhs: Zero, rhs: Zero) -> Bool { return true }
}
public typealias One = Succ<Zero>
public typealias Two = Succ<One>
@Kuniwak
Kuniwak / XCTContextPached.swift
Created Aug 7, 2018
Workaround for XCTContext.runActivity on AppCode.
View XCTContextPached.swift
import _SwiftXCTestOverlayShims
public extension XCTContext {
// XXX: This is for AppCode. The original of runActivity have been failed on only AppCode.
// This cause is __XCTContextShouldStartActivity, it returns true when it is called on Xcode, but not on AppCode.
public class func runActivityPatched<Result>(named name: String, block: (XCTActivity) throws -> Result) rethrows -> Result {
let context = _XCTContextCurrent()
return try autoreleasepool {
let activity = _XCTContextWillStartActivity(context, name, XCTActivityTypeUserCreated)
@Kuniwak
Kuniwak / all_your_vim_are_belong_to_us.txt
Last active Mar 23, 2018
ALL YOUR VIM ARE BELONG TO US 【推奨環境】background=dark guifont=SourceCodePro-Regular
View all_your_vim_are_belong_to_us.txt
..
.::::.
___________ :;;;;:`____________
\_________/ ?????L \__________/
|.....| ????????> :.......'
|:::::| $$$$$$"`.:::::::' ,
,|:::::| $$$$"`.:::::::' .OOS.
,7D|;;;;;| $$"`.;;;;;;;' .OOO888S.
.GDDD|;;;;;| ?`.;;;;;;;' .OO8DDDDDNNS.
'DDO|IIIII| .7IIIII7' .DDDDDDDDNNNF`
You can’t perform that action at this time.