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">> }
View stupid_verification_approach.md

やりたいこと

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

疑問

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

超雑な例

@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 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> };
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 / SE0176Tests.swift
Last active Jan 25, 2018
SE-0176 の理解を確認するための例題集です
View SE0176Tests.swift
// 問題: コンパイルエラーもしくは実行時警告になる testX 関数をすべて答えてください。
import XCTest
class SE0176PlaygroundTests: XCTestCase {
func test1() {
struct ExampleStruct {
mutating func assignedBy(_ block: () -> ExampleStruct) {
self = block()
View kitchen-dianose-error.md
$ ruby --version
ruby 2.3.3p222 (2016-11-21 revision 56859) [x86_64-darwin16]

$ bundle list | grep kitchen
  * kitchen-ansible (0.45.9)
  * kitchen-vagrant (1.0.1)
  * test-kitchen (1.15.0)
You can’t perform that action at this time.