Kuniwak

theory "Well_Not_Dense_Order" imports Main begin
context wellorder
begin

definition bot :: 'a
  where "bot ≡ LEAST x. True"

sublocale order_bot bot less_eq less
proof standard
  fix a

Kuniwak

theory "Well_Dense_Order" imports Main begin

datatype a = A

text "a は整列順序である。"
instantiation a :: wellorder
begin

definition less_eq_a :: "a ⇒ a ⇒ bool"
  where "less_eq_a a b ≡ True"

Kuniwak

theorem
  fixes f :: "'x ⇒ 'y ⇒ 'y"
  assumes finite: "finite X"
    and eq: "⋀x. x ∈ X ⟹ f x = g x"
  shows "Finite_Set.fold f z X = Finite_Set.fold g z X"
using finite using eq by (rule_tac fold_closed_eq[where ?B=UNIV]; simp)

Kuniwak

Before

$ sw_vers
ProductName:	Mac OS X
ProductVersion:	10.14.5
BuildVersion:	18F132

$ xcodebuild -version
Xcode 10.2.1

Kuniwak

--- appium-base-driver/lib/express/server.js    2019-07-17 12:37:19.000000000 +0900
+++ appium-base-driver/lib/express/server.js    2019-07-17 12:37:49.000000000 +0900
@@ -49,7 +49,7 @@ async function server (configureRoutes, 
       reject(err);
     });
     httpServer.on('connection', (socket) => {
-      socket.setTimeout(600 * 1000); // 10 minute timeout
+      socket.setTimeout(600 * 10000); // 10 minute timeout
       socket.on('error', reject);
     });

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: