Kuniwak

----------------------------- MODULE playground -----------------------------

VARIABLES varTable

\* Initial Predicate:
Init == varTable = { <<0, "a">>, <<1, "b">> }

\* Next-state relation:
Next == varTable' = { <<2, "c">> }

Kuniwak

やりたいこと

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

疑問

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

超雑な例

Kuniwak

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)

Kuniwak

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

public enum Result<T, E> {
    case success(T)
    case failure(because: E)


    public var isSuccess: Bool {
        switch self {
        case .success:
            return true
        case .failure:

Kuniwak

%{
number_of_generated = 5
}%


public struct PrefixedArray<Element, RestElements> {
    public let prefix: Element
    public let rest: RestElements

Kuniwak

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

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

// 問題: コンパイルエラーもしくは実行時警告になる testX 関数をすべて答えてください。

import XCTest


class SE0176PlaygroundTests: XCTestCase {
    func test1() {
        struct ExampleStruct {
            mutating func assignedBy(_ block: () -> ExampleStruct) {
                self = block()

Kuniwak

自己紹介

SET（Software Engineer in Test） のグループの元マネージャ。専門は ソフトウェアテスト/Lint/Git。実務経験のあるプログラミング言語は JavaScript, TypeScript, Swift, C#, Go, Isabelle, OCaml, F#（コードは OSS を参照）。

（2025/12 現在）転職活動はしていません。

提供できる価値