y-taka-23

.    
.
.    
.    
. 
. 	
.	 			 
.    						
.	  	
.	  		

y-taka-23

// ************************************
//   群のモデル
// ************************************

// ------------------------------------
//   群の公理
// ------------------------------------

// 群の元
sig Element {

y-taka-23

// ************************************
//   組み合わせ回路のモデル
// ************************************

// ------------------------------------
//   組み合わせ回路の性質
// ------------------------------------

// 回路の構成要素
abstract sig Element {

y-taka-23

// ************************************
//   Git のコミットグラフのモデル
// ************************************

open util/ordering[Time]

// ------------------------------------
//   グラフの構成要素
// ------------------------------------

y-taka-23

// ************************************
//   十進法による符号なし整数演算のモデル
// ************************************

open util/ordering[Position]

// ------------------------------------
//   位取り記数法のモデリング
// ------------------------------------

y-taka-23

Section Perceptron.

Require Import QArith List.

Inductive Q_vector : nat -> Set :=
    | vnil  : Q_vector O
    | vcons : forall n : nat,
              Q -> Q_vector n -> Q_vector (S n).
Implicit Arguments vcons [n].
Notation "x ; v" := (vcons x v)

y-taka-23

// ************************************
//   ジュースの自動販売機のモデル
// ************************************

open util/ordering[Time]

// 時刻パラメータ
sig Time {}

// 簡略化のため、コインの額面とジュースの種類はそれぞれ 1 種類とする

y-taka-23

(*******************************************************)
(** //// Validation of the Stack Machine Compiler //// *)
(*******************************************************)

Require Import List.

(* Definition : Identifiers *)
Inductive id : Type :=
    | Id : nat -> id.

y-taka-23

Require Import Ascii String.
Open Scope string_scope.
Definition Q : string := "
Eval compute in ""
Require Import Ascii String.
Open Scope string_scope.
Definition Q : string := "" ++ """" ++ Q ++ """" ++ ""."" ++ Q.".
Eval compute in "
Require Import Ascii String.
Open Scope string_scope.

y-taka-23

(******************************************************)
(** //// Validation of the Quick Sort ////            *)
(******************************************************)

Section QuickSort.

Require Import Arith List.
Require Import Recdef.
Require Import Sorting.Sorted Sorting.Permutation.