products/Sources/formale Sprachen/Coq/theories/Strings/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: xts765.cob   Sprache: Coq

Untersuchung Coq©
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import Ascii Basics Bvector String Vector.
Export VectorNotations.
Open Scope program_scope.
Open Scope string_scope.

Definition ByteVector := Vector.t ascii.

Definition ByteNil : ByteVector 0 := Vector.nil ascii.

Definition little_endian_to_string {n : nat} (v : ByteVector n) : string :=
  fold_right String v "".

Definition to_string {n : nat} : ByteVector n -> string :=
  little_endian_to_string ∘ rev.

Fixpoint little_endian_of_string (s : string) : ByteVector (length s) :=
  match s with
  | "" => ByteNil
  | String b s' => b :: little_endian_of_string s'
  end.

Definition of_string (s : string) : ByteVector (length s) :=
  rev (little_endian_of_string s).

Fixpoint to_Bvector {n : nat} (v : ByteVector n) : Bvector (n * 8) :=
  match v with
  | [] => []
  | Ascii b0 b1 b2 b3 b4 b5 b6 b7::v' =>
    b0::b1::b2::b3::b4::b5::b6::b7::to_Bvector v'
  end.

Fixpoint of_Bvector {n : nat} : Bvector (n * 8) -> ByteVector n :=
  match n with
  | 0 => fun _ => []
  | S n' =>
    fun v =>
      let (b0, v1) := uncons v in
      let (b1, v2) := uncons v1 in
      let (b2, v3) := uncons v2 in
      let (b3, v4) := uncons v3 in
      let (b4, v5) := uncons v4 in
      let (b5, v6) := uncons v5 in
      let (b6, v7) := uncons v6 in
      let (b7, v8) := uncons v7 in
      Ascii b0 b1 b2 b3 b4 b5 b6 b7::of_Bvector v8
  end.

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.23Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff