From 7cc748edaf023f533b74c582824a5fa2c2ccfa10 Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre Date: Tue, 21 Jun 2011 11:33:14 +0200 Subject: [PATCH] restored insertion sort proof (my mistake) --- ...ertionSort_WP_parameter insertion_sort_1.v | 203 ++++++++++++++++++ ...ertionSort_WP_parameter insertion_sort_2.v | 193 +++++++++++++++++ .../programs/insertion_sort/why3session.xml | 202 +++++++++++++++++ 3 files changed, 598 insertions(+) create mode 100644 examples/programs/insertion_sort/insertion_sort.mlw_InsertionSort_WP_parameter insertion_sort_1.v create mode 100644 examples/programs/insertion_sort/insertion_sort.mlw_InsertionSort_WP_parameter insertion_sort_2.v create mode 100644 examples/programs/insertion_sort/why3session.xml diff --git a/examples/programs/insertion_sort/insertion_sort.mlw_InsertionSort_WP_parameter insertion_sort_1.v b/examples/programs/insertion_sort/insertion_sort.mlw_InsertionSort_WP_parameter insertion_sort_1.v new file mode 100644 index 000000000..5869df9a9 --- /dev/null +++ b/examples/programs/insertion_sort/insertion_sort.mlw_InsertionSort_WP_parameter insertion_sort_1.v @@ -0,0 +1,203 @@ +(* This file is generated by Why3's Coq driver *) +(* Beware! Only edit allowed sections below *) +Require Import ZArith. +Require Import Rbase. +Definition unit := unit. + +Parameter label : Type. + +Parameter at1: forall (a:Type), a -> label -> a. + +Implicit Arguments at1. + +Parameter old: forall (a:Type), a -> a. + +Implicit Arguments old. + +Inductive ref (a:Type) := + | mk_ref : a -> ref a. +Implicit Arguments mk_ref. + +Definition contents (a:Type)(u:(ref a)): a := + match u with + | mk_ref contents1 => contents1 + end. +Implicit Arguments contents. + +Parameter map : forall (a:Type) (b:Type), Type. + +Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b. + +Implicit Arguments get. + +Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b). + +Implicit Arguments set. + +Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)), + forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1) + a2) = b1). + +Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)), + forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) + a2) = (get m a2)). + +Parameter const: forall (b:Type) (a:Type), b -> (map a b). + +Set Contextual Implicit. +Implicit Arguments const. +Unset Contextual Implicit. + +Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const( + b1):(map a b)) a1) = b1). + +Inductive array (a:Type) := + | mk_array : Z -> (map Z a) -> array a. +Implicit Arguments mk_array. + +Definition elts (a:Type)(u:(array a)): (map Z a) := + match u with + | mk_array _ elts1 => elts1 + end. +Implicit Arguments elts. + +Definition length (a:Type)(u:(array a)): Z := + match u with + | mk_array length1 _ => length1 + end. +Implicit Arguments length. + +Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i). +Implicit Arguments get1. + +Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) := + match a1 with + | mk_array xcl0 _ => (mk_array xcl0 (set (elts a1) i v)) + end. +Implicit Arguments set1. + +Definition sorted_sub(a:(map Z Z)) (l:Z) (u:Z): Prop := forall (i1:Z) (i2:Z), + (((l <= i1)%Z /\ (i1 <= i2)%Z) /\ (i2 < u)%Z) -> ((get a i1) <= (get a + i2))%Z. + +Definition sorted_sub1(a:(array Z)) (l:Z) (u:Z): Prop := (sorted_sub (elts a) + l u). + +Definition sorted(a:(array Z)): Prop := (sorted_sub (elts a) 0%Z (length a)). + +Definition map_eq_sub (a:Type)(a1:(map Z a)) (a2:(map Z a)) (l:Z) + (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((get a1 + i) = (get a2 i)). +Implicit Arguments map_eq_sub. + +Definition exchange (a:Type)(a1:(map Z a)) (a2:(map Z a)) (i:Z) + (j:Z): Prop := ((get a1 i) = (get a2 j)) /\ (((get a2 i) = (get a1 j)) /\ + forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((get a1 k) = (get a2 k))). +Implicit Arguments exchange. + +Axiom exchange_set : forall (a:Type), forall (a1:(map Z a)), forall (i:Z) + (j:Z), (exchange a1 (set (set a1 i (get a1 j)) j (get a1 i)) i j). + +Inductive permut_sub{a:Type} : (map Z a) -> (map Z a) -> Z -> Z -> Prop := + | permut_refl : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z), + (map_eq_sub a1 a2 l u) -> (permut_sub a1 a2 l u) + | permut_sym : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z), + (permut_sub a1 a2 l u) -> (permut_sub a2 a1 l u) + | permut_trans : forall (a1:(map Z a)) (a2:(map Z a)) (a3:(map Z a)), + forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> ((permut_sub a2 a3 l + u) -> (permut_sub a1 a3 l u)) + | permut_exchange : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) + (u:Z) (i:Z) (j:Z), ((l <= i)%Z /\ (i < u)%Z) -> (((l <= j)%Z /\ + (j < u)%Z) -> ((exchange a1 a2 i j) -> (permut_sub a1 a2 l u))). +Implicit Arguments permut_sub. + +Axiom permut_weakening : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z + a)), forall (l1:Z) (r1:Z) (l2:Z) (r2:Z), (((l1 <= l2)%Z /\ (l2 <= r2)%Z) /\ + (r2 <= r1)%Z) -> ((permut_sub a1 a2 l2 r2) -> (permut_sub a1 a2 l1 r1)). + +Axiom permut_eq : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z a)), + forall (l:Z) (u:Z), (l <= u)%Z -> ((permut_sub a1 a2 l u) -> forall (i:Z), + ((i < l)%Z \/ (u <= i)%Z) -> ((get a2 i) = (get a1 i))). + +Axiom permut_exists : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z a)), + forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z), ((l <= i)%Z /\ + (i < u)%Z) -> exists j:Z, ((l <= j)%Z /\ (j < u)%Z) /\ ((get a2 + i) = (get a1 j)). + +Definition exchange1 (a:Type)(a1:(array a)) (a2:(array a)) (i:Z) + (j:Z): Prop := (exchange (elts a1) (elts a2) i j). +Implicit Arguments exchange1. + +Definition permut_sub1 (a:Type)(a1:(array a)) (a2:(array a)) (l:Z) + (u:Z): Prop := (permut_sub (elts a1) (elts a2) l u). +Implicit Arguments permut_sub1. + +Definition permut (a:Type)(a1:(array a)) (a2:(array a)): Prop := + ((length a1) = (length a2)) /\ (permut_sub (elts a1) (elts a2) 0%Z + (length a1)). +Implicit Arguments permut. + +Axiom exchange_permut : forall (a:Type), forall (a1:(array a)) (a2:(array a)) + (i:Z) (j:Z), (exchange1 a1 a2 i j) -> (((length a1) = (length a2)) -> + (((0%Z <= i)%Z /\ (i < (length a1))%Z) -> (((0%Z <= j)%Z /\ + (j < (length a1))%Z) -> (permut a1 a2)))). + +Definition array_eq_sub (a:Type)(a1:(array a)) (a2:(array a)) (l:Z) + (u:Z): Prop := (map_eq_sub (elts a1) (elts a2) l u). +Implicit Arguments array_eq_sub. + +Definition array_eq (a:Type)(a1:(array a)) (a2:(array a)): Prop := + ((length a1) = (length a2)) /\ (array_eq_sub a1 a2 0%Z (length a1)). +Implicit Arguments array_eq. + +Axiom array_eq_sub_permut : forall (a:Type), forall (a1:(array a)) (a2:(array + a)) (l:Z) (u:Z), (array_eq_sub a1 a2 l u) -> (permut_sub1 a1 a2 l u). + +Axiom array_eq_permut : forall (a:Type), forall (a1:(array a)) (a2:(array + a)), (array_eq a1 a2) -> (permut a1 a2). + +Theorem WP_parameter_insertion_sort : forall (a:Z), forall (a1:(map Z Z)), + let a2 := (mk_array a a1) in ((1%Z <= (a - 1%Z)%Z)%Z -> forall (a3:(map Z + Z)), let a4 := (mk_array a a3) in forall (i:Z), ((1%Z <= i)%Z /\ + (i <= (a - 1%Z)%Z)%Z) -> (((sorted_sub a3 0%Z i) /\ (permut a4 a2)) -> + (((0%Z <= i)%Z /\ (i < a)%Z) -> let result := (get a3 i) in + ((((0%Z <= i)%Z /\ (i <= i)%Z) /\ ((permut (set1 a4 i result) a2) /\ + ((forall (k1:Z) (k2:Z), (((0%Z <= k1)%Z /\ (k1 <= k2)%Z) /\ (k2 <= i)%Z) -> + ((~ (k1 = i)) -> ((~ (k2 = i)) -> ((get a3 k1) <= (get a3 k2))%Z))) /\ + forall (k:Z), (((i + 1%Z)%Z <= k)%Z /\ (k <= i)%Z) -> (result < (get a3 + k))%Z))) -> forall (j:Z), forall (a5:(map Z Z)), let a6 := (mk_array a + a5) in ((((0%Z <= j)%Z /\ (j <= i)%Z) /\ ((permut (set1 a6 j result) a2) /\ + ((forall (k1:Z) (k2:Z), (((0%Z <= k1)%Z /\ (k1 <= k2)%Z) /\ (k2 <= i)%Z) -> + ((~ (k1 = j)) -> ((~ (k2 = j)) -> ((get a5 k1) <= (get a5 k2))%Z))) /\ + forall (k:Z), (((j + 1%Z)%Z <= k)%Z /\ (k <= i)%Z) -> (result < (get a5 + k))%Z))) -> ((0%Z < j)%Z -> (((0%Z <= (j - 1%Z)%Z)%Z /\ + ((j - 1%Z)%Z < a)%Z) -> ((result < (get a5 (j - 1%Z)%Z))%Z -> + (((0%Z <= (j - 1%Z)%Z)%Z /\ ((j - 1%Z)%Z < a)%Z) -> (((0%Z <= j)%Z /\ + (j < a)%Z) -> forall (a7:(map Z Z)), let a8 := (mk_array a a7) in + ((a7 = (set a5 j (get a5 (j - 1%Z)%Z))) -> ((exchange match (set1 a8 + (j - 1%Z)%Z result) with + | mk_array _ elts1 => elts1 + end match (set1 a6 j result) with + | mk_array _ elts1 => elts1 + end (j - 1%Z)%Z j) -> forall (j1:Z), (j1 = (j - 1%Z)%Z) -> (permut (set1 a8 + j1 result) a2))))))))))))). +(* YOU MAY EDIT THE PROOF BELOW *) +intuition. +intuition. +unfold set1. +unfold permut. +split. +simpl. +auto. +apply permut_trans with (elts (set1 (mk_array a a5) j (get a3 i))); auto. +subst j1. +apply permut_exchange with (j-1)%Z j. +simpl; omega. +simpl; omega. +assumption. +unfold permut in H17. +intuition. +Qed. +(* DO NOT EDIT BELOW *) + + diff --git a/examples/programs/insertion_sort/insertion_sort.mlw_InsertionSort_WP_parameter insertion_sort_2.v b/examples/programs/insertion_sort/insertion_sort.mlw_InsertionSort_WP_parameter insertion_sort_2.v new file mode 100644 index 000000000..4387b2184 --- /dev/null +++ b/examples/programs/insertion_sort/insertion_sort.mlw_InsertionSort_WP_parameter insertion_sort_2.v @@ -0,0 +1,193 @@ +(* This file is generated by Why3's Coq driver *) +(* Beware! Only edit allowed sections below *) +Require Import ZArith. +Require Import Rbase. +Definition unit := unit. + +Parameter label : Type. + +Parameter at1: forall (a:Type), a -> label -> a. + +Implicit Arguments at1. + +Parameter old: forall (a:Type), a -> a. + +Implicit Arguments old. + +Inductive ref (a:Type) := + | mk_ref : a -> ref a. +Implicit Arguments mk_ref. + +Definition contents (a:Type)(u:(ref a)): a := + match u with + | mk_ref contents1 => contents1 + end. +Implicit Arguments contents. + +Parameter map : forall (a:Type) (b:Type), Type. + +Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b. + +Implicit Arguments get. + +Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b). + +Implicit Arguments set. + +Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)), + forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1) + a2) = b1). + +Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)), + forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) + a2) = (get m a2)). + +Parameter const: forall (b:Type) (a:Type), b -> (map a b). + +Set Contextual Implicit. +Implicit Arguments const. +Unset Contextual Implicit. + +Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const( + b1):(map a b)) a1) = b1). + +Inductive array (a:Type) := + | mk_array : Z -> (map Z a) -> array a. +Implicit Arguments mk_array. + +Definition elts (a:Type)(u:(array a)): (map Z a) := + match u with + | mk_array _ elts1 => elts1 + end. +Implicit Arguments elts. + +Definition length (a:Type)(u:(array a)): Z := + match u with + | mk_array length1 _ => length1 + end. +Implicit Arguments length. + +Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i). +Implicit Arguments get1. + +Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) := + match a1 with + | mk_array xcl0 _ => (mk_array xcl0 (set (elts a1) i v)) + end. +Implicit Arguments set1. + +Definition sorted_sub(a:(map Z Z)) (l:Z) (u:Z): Prop := forall (i1:Z) (i2:Z), + (((l <= i1)%Z /\ (i1 <= i2)%Z) /\ (i2 < u)%Z) -> ((get a i1) <= (get a + i2))%Z. + +Definition sorted_sub1(a:(array Z)) (l:Z) (u:Z): Prop := (sorted_sub (elts a) + l u). + +Definition sorted(a:(array Z)): Prop := (sorted_sub (elts a) 0%Z (length a)). + +Definition map_eq_sub (a:Type)(a1:(map Z a)) (a2:(map Z a)) (l:Z) + (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((get a1 + i) = (get a2 i)). +Implicit Arguments map_eq_sub. + +Definition exchange (a:Type)(a1:(map Z a)) (a2:(map Z a)) (i:Z) + (j:Z): Prop := ((get a1 i) = (get a2 j)) /\ (((get a2 i) = (get a1 j)) /\ + forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((get a1 k) = (get a2 k))). +Implicit Arguments exchange. + +Axiom exchange_set : forall (a:Type), forall (a1:(map Z a)), forall (i:Z) + (j:Z), (exchange a1 (set (set a1 i (get a1 j)) j (get a1 i)) i j). + +Inductive permut_sub{a:Type} : (map Z a) -> (map Z a) -> Z -> Z -> Prop := + | permut_refl : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z), + (map_eq_sub a1 a2 l u) -> (permut_sub a1 a2 l u) + | permut_sym : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z), + (permut_sub a1 a2 l u) -> (permut_sub a2 a1 l u) + | permut_trans : forall (a1:(map Z a)) (a2:(map Z a)) (a3:(map Z a)), + forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> ((permut_sub a2 a3 l + u) -> (permut_sub a1 a3 l u)) + | permut_exchange : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) + (u:Z) (i:Z) (j:Z), ((l <= i)%Z /\ (i < u)%Z) -> (((l <= j)%Z /\ + (j < u)%Z) -> ((exchange a1 a2 i j) -> (permut_sub a1 a2 l u))). +Implicit Arguments permut_sub. + +Axiom permut_weakening : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z + a)), forall (l1:Z) (r1:Z) (l2:Z) (r2:Z), (((l1 <= l2)%Z /\ (l2 <= r2)%Z) /\ + (r2 <= r1)%Z) -> ((permut_sub a1 a2 l2 r2) -> (permut_sub a1 a2 l1 r1)). + +Axiom permut_eq : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z a)), + forall (l:Z) (u:Z), (l <= u)%Z -> ((permut_sub a1 a2 l u) -> forall (i:Z), + ((i < l)%Z \/ (u <= i)%Z) -> ((get a2 i) = (get a1 i))). + +Axiom permut_exists : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z a)), + forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z), ((l <= i)%Z /\ + (i < u)%Z) -> exists j:Z, ((l <= j)%Z /\ (j < u)%Z) /\ ((get a2 + i) = (get a1 j)). + +Definition exchange1 (a:Type)(a1:(array a)) (a2:(array a)) (i:Z) + (j:Z): Prop := (exchange (elts a1) (elts a2) i j). +Implicit Arguments exchange1. + +Definition permut_sub1 (a:Type)(a1:(array a)) (a2:(array a)) (l:Z) + (u:Z): Prop := (permut_sub (elts a1) (elts a2) l u). +Implicit Arguments permut_sub1. + +Definition permut (a:Type)(a1:(array a)) (a2:(array a)): Prop := + ((length a1) = (length a2)) /\ (permut_sub (elts a1) (elts a2) 0%Z + (length a1)). +Implicit Arguments permut. + +Axiom exchange_permut : forall (a:Type), forall (a1:(array a)) (a2:(array a)) + (i:Z) (j:Z), (exchange1 a1 a2 i j) -> (((length a1) = (length a2)) -> + (((0%Z <= i)%Z /\ (i < (length a1))%Z) -> (((0%Z <= j)%Z /\ + (j < (length a1))%Z) -> (permut a1 a2)))). + +Definition array_eq_sub (a:Type)(a1:(array a)) (a2:(array a)) (l:Z) + (u:Z): Prop := (map_eq_sub (elts a1) (elts a2) l u). +Implicit Arguments array_eq_sub. + +Definition array_eq (a:Type)(a1:(array a)) (a2:(array a)): Prop := + ((length a1) = (length a2)) /\ (array_eq_sub a1 a2 0%Z (length a1)). +Implicit Arguments array_eq. + +Axiom array_eq_sub_permut : forall (a:Type), forall (a1:(array a)) (a2:(array + a)) (l:Z) (u:Z), (array_eq_sub a1 a2 l u) -> (permut_sub1 a1 a2 l u). + +Axiom array_eq_permut : forall (a:Type), forall (a1:(array a)) (a2:(array + a)), (array_eq a1 a2) -> (permut a1 a2). + +Theorem WP_parameter_insertion_sort : forall (a:Z), forall (a1:(map Z Z)), + let a2 := (mk_array a a1) in ((1%Z <= (a - 1%Z)%Z)%Z -> forall (a3:(map Z + Z)), let a4 := (mk_array a a3) in forall (i:Z), ((1%Z <= i)%Z /\ + (i <= (a - 1%Z)%Z)%Z) -> (((sorted_sub a3 0%Z i) /\ (permut a4 a2)) -> + (((0%Z <= i)%Z /\ (i < a)%Z) -> let result := (get a3 i) in + ((((0%Z <= i)%Z /\ (i <= i)%Z) /\ ((permut (set1 a4 i result) a2) /\ + ((forall (k1:Z) (k2:Z), (((0%Z <= k1)%Z /\ (k1 <= k2)%Z) /\ (k2 <= i)%Z) -> + ((~ (k1 = i)) -> ((~ (k2 = i)) -> ((get a3 k1) <= (get a3 k2))%Z))) /\ + forall (k:Z), (((i + 1%Z)%Z <= k)%Z /\ (k <= i)%Z) -> (result < (get a3 + k))%Z))) -> forall (j:Z), forall (a5:(map Z Z)), let a6 := (mk_array a + a5) in ((((0%Z <= j)%Z /\ (j <= i)%Z) /\ ((permut (set1 a6 j result) a2) /\ + ((forall (k1:Z) (k2:Z), (((0%Z <= k1)%Z /\ (k1 <= k2)%Z) /\ (k2 <= i)%Z) -> + ((~ (k1 = j)) -> ((~ (k2 = j)) -> ((get a5 k1) <= (get a5 k2))%Z))) /\ + forall (k:Z), (((j + 1%Z)%Z <= k)%Z /\ (k <= i)%Z) -> (result < (get a5 + k))%Z))) -> ((0%Z < j)%Z -> (((0%Z <= (j - 1%Z)%Z)%Z /\ + ((j - 1%Z)%Z < a)%Z) -> ((result < (get a5 (j - 1%Z)%Z))%Z -> + (((0%Z <= (j - 1%Z)%Z)%Z /\ ((j - 1%Z)%Z < a)%Z) -> (((0%Z <= j)%Z /\ + (j < a)%Z) -> forall (a7:(map Z Z)), (a7 = (set a5 j (get a5 + (j - 1%Z)%Z))) -> ((exchange match (set1 (mk_array a a7) (j - 1%Z)%Z + result) with + | mk_array _ elts1 => elts1 + end match (set1 a6 j result) with + | mk_array _ elts1 => elts1 + end (j - 1%Z)%Z j) -> forall (j1:Z), (j1 = (j - 1%Z)%Z) -> forall (k1:Z) + (k2:Z), (((0%Z <= k1)%Z /\ (k1 <= k2)%Z) /\ (k2 <= i)%Z) -> + ((~ (k1 = j1)) -> ((~ (k2 = j1)) -> ((get a7 k1) <= (get a7 + k2))%Z))))))))))))). +(* YOU MAY EDIT THE PROOF BELOW *) +intuition. +intuition. + +Qed. +(* DO NOT EDIT BELOW *) + + diff --git a/examples/programs/insertion_sort/why3session.xml b/examples/programs/insertion_sort/why3session.xml new file mode 100644 index 000000000..b2d767676 --- /dev/null +++ b/examples/programs/insertion_sort/why3session.xml @@ -0,0 +1,202 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + -- GitLab