Skip to content

Instantly share code, notes, and snippets.

TAKAHASHI Yuto y-taka-23

Block or report user

Report or block y-taka-23

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
@y-taka-23
y-taka-23 / Sample.hs
Created Dec 24, 2016
Samples of Verification by LiquidHaskell
View Sample.hs
module Sample where
import Language.Haskell.Liquid.Prelude ( liquidError )
{-@ safeHead :: { xs:[a] | len xs > 0 } -> a @-}
safeHead [] = liquidError "empty list"
safeHead (x : _) = x
-- badUsage = safeHead [] -- => Liquid Type Mismatch
@y-taka-23
y-taka-23 / alloy_kubernetes.als
Last active Dec 19, 2016
Alloy による Kubernetes のコンテナスケジューリングのモデリング
View alloy_kubernetes.als
open util/ordering[Time]
sig Time {}
abstract sig Event {
pre, post : Time,
} {
post = pre.next
}
@y-taka-23
y-taka-23 / alloy_sequent.als
Last active Dec 23, 2015
Alloy による命題論理のシークエント計算のモデリング
View alloy_sequent.als
// ************************************
// 命題論理のシークエント計算のモデル
// ************************************
// 論理式
abstract sig Formula {}
// 原子命題
sig Atom extends Formula {}
@y-taka-23
y-taka-23 / alloy_aws_security_group.als
Created Dec 6, 2015
Alloy による AWS セキュリティグループのモデリング
View alloy_aws_security_group.als
// **************************************************
// AWS セキュリティグループのモデル
// **************************************************
// 通信プロトコル
enum Protocol { TCP, UDP, ICMP }
// 通信ポート
sig Port {}
@y-taka-23
y-taka-23 / coq_uniq.v
Created Sep 12, 2015
An Implementation of the uniq Command Certified by Coq
View coq_uniq.v
Parameter A : Type.
Parameter beq_A : A -> A -> bool.
Section Uniq.
Require Import Arith List.
Hypothesis beq_A_true : forall x y : A,
beq_A x y = true -> x = y.
Hypothesis beq_A_false : forall x y : A,
@y-taka-23
y-taka-23 / promela_sharing.pml
Created Dec 14, 2014
An Invalid (Deadlocked) Model of Resource Sharing Problem
View promela_sharing.pml
/*
* Resource Sharing Problem (Example for Deadlock)
*/
mtype = { LOCK, UNLOCK };
proctype Client(chan to_res1, to_res2) {
if
:: to_res1 ! LOCK(_pid);
to_res2 ! LOCK(_pid);
@y-taka-23
y-taka-23 / death_march_05.cob
Last active Aug 29, 2015
CodeIQ「第 5 回デスマコロシアム」の固定形式 COBOL 85 による実装
View death_march_05.cob
IDENTIFICATION DIVISION.
PROGRAM-ID. DEATH-MARCH-05.
DATA DIVISION.
WORKING-STORAGE SECTION.
77 FB-STR PIC X(153).
77 CNT PIC 9(2) VALUE 1.
77 QUOT PIC 9(2).
77 REM-3 PIC 9(1).
77 REM-5 PIC 9(1).
@y-taka-23
y-taka-23 / fibonacci.cob
Created Jul 27, 2014
COBOL による Fibonacci 数の計算
View fibonacci.cob
IDENTIFICATION DIVISION.
PROGRAM-ID. FIBONACCI.
DATA DIVISION.
WORKING-STORAGE SECTION.
01 ARGUMENT PIC 9(2).
01 RETURN-VALUE PIC 9(25).
01 RESULT PIC Z(25).
01 DP-TABLE.
03 VALS PIC 9(25) OCCURS 99.
@y-taka-23
y-taka-23 / rnpcalc.cob
Last active Aug 29, 2015
COBOL による逆ポーランド電卓
View rnpcalc.cob
IDENTIFICATION DIVISION.
PROGRAM-ID. RNPCALC.
DATA DIVISION.
WORKING-STORAGE SECTION.
01 STACK-POS PIC 9(2) VALUE 1.
01 STACK.
03 STACK-DATA PIC 9(4) OCCURS 10 VALUE 0.
01 EXPR PIC X(20).
01 EXPR-POS PIC 9(2).
@y-taka-23
y-taka-23 / promela_leader.pml
Last active Jan 4, 2016
A Model of Leader Election on Promela/SPIN
View promela_leader.pml
/*
* Leader Election by Chang-Roberts Algorithm
*/
byte leader = 0; /* number of leaders */
proctype Node(chan ch_in, ch_out) {
byte tok;
You can’t perform that action at this time.