Skip to content

Instantly share code, notes, and snippets.

View Kuniwak's full-sized avatar
💭
I may be slow to respond.

Yuki Kokubun Kuniwak

💭
I may be slow to respond.
213 followers · 1 following
View GitHub Profile
@Kuniwak
Kuniwak / NumberGenerator3.FromGPT4.cs
Created February 12, 2024 09:22
全体は https://gist.github.com/Kuniwak/53ea12ff871b531bd1445a504ac55e4e にあります。
// https://chat.openai.com/share/a75ee402-3131-4ee8-9a9d-54bf1b81071c
using System;
namespace Playground.CopilotTDD.Tests
{
public static class NumberGenerator
{
public static int GetBetween0To100BySeed(int seed)
{
// 線形合同法のパラメータ
@Kuniwak
Kuniwak / NumberGenerator1.FromGitHubCopilot.cs
Last active February 12, 2024 09:23
GitHub Copilot に [0-100) の区間でその分布が正規分布に従う関数を実装させてみた実験例
namespace Playground.CopilotTDD;
public static class NumberGenerator
{
public static int GetBetween0To100BySeed(int seed)
{
return new Random(seed).Next(0, 100);
}
}
@Kuniwak
Kuniwak / Sceratch.thy
Created August 31, 2023 07:31
https://vim-jp.slack.com/archives/C01844Y1FD2/p1693376299215649
theory Scratch
imports Main
begin
no_notation relcomp (infixr "O" 75)
(* oreo 型の内部表現 *)
datatype oreo0 = O0 | Ore0 oreo0 | Reo0 oreo0
@Kuniwak
Kuniwak / Well_Not_Dense_Order.thy
Created July 15, 2022 01:01
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
Kuniwak / Well_Dense_Order.thy
Created July 15, 2022 00:39
整列順序で稠密順序な例。
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
Kuniwak / FiniteSet_fold.thy
Last active August 28, 2021 00:33
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
Kuniwak / build-logs.md
Created July 21, 2019 04:12

Before

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

$ xcodebuild -version
Xcode 10.2.1
@Kuniwak
Kuniwak / longer-timeout.patch
Created July 18, 2019 08:12
--- 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
Kuniwak / 1-playground.tla
Last active May 27, 2019 08:46
解決しました（コメント参照） ~~なぜ、Temporal properties were violated になるのかわかりません。。。~~
----------------------------- MODULE playground -----------------------------
VARIABLES varTable
\* Initial Predicate:
Init == varTable = { <<0, "a">>, <<1, "b">> }
\* Next-state relation:
Next == varTable' = { <<2, "c">> }
@Kuniwak
Kuniwak / stupid_verification_approach.md
Last active March 2, 2019 08:57

やりたいこと

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

疑問

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

超雑な例