.V Dateiendung

Entwicklerdatei, die von Coq verwendet wird, einer Anwendung zur Entwicklung mathematischer Beweise; sie wird in einem Textformat gespeichert und enthält Quellcode, der in der Sprache Gallina erstellt wurde, die auf einer ausdrucksstarken formalen Sprache namens Kalkül der induktiven Konstruktionen (CIC) basiert; sie wird zum Speichern mathematischer Beweise verwendet.

Entwickler geben Ausdrücke in V-Dateien mithilfe des „Vernakulars“ von Gallina an. Dabei handelt es sich um die Syntax oder Befehlssprache der Sprache Gallina. Sobald V-Dateien geschrieben wurden, können sie mit der Coq Proof Assistant integrierten Entwicklungsumgebung kompiliert und ausgeführt werden, deren Programmname CoqIDE lautet.

HINWEIS: Die Entwicklung von Coq, die zuvor vom The Coq Development Team betreut wurde, wird nun von ADT Coq betreut. ADT steht für „Action for Technological Development.“

Eine V-Datei enthält Quellcode, der in der Programmiersprache V geschrieben wurde. Typischerweise enthält eine V-Datei ein V-Programm oder -Modul.

Sie können eine V-Datei öffnen und ihren Inhalt mit einem beliebigen Text- oder Quellcodeeditor bearbeiten. Quellcodeeditoren wie Microsoft Visual Studio Code und GitHub Atom enthalten hilfreiche Werkzeuge, die das Lesen und Bearbeiten von V-Dateien erleichtern.

Wenn Ihre V-Datei ein Programm enthält, können Sie das Programm mit dem Befehl run von V ausführen.

Unbearbeitete „V“-Bilddatei, die von ppmtoyuvsplit erstellt wird, einem Unix-basierten Programm zum Aufteilen von Portable-PixMap-Bildern (.PPM-Dateien) in .Y, .U und V-Dateien; speichert die „V“-Chrominanz- bzw. Farbkomponente des Bildes; kann mit dem Dienstprogramm yuvsplittoppm wieder in die ursprüngliche PPM-Datei zurückgewandelt werden.

V-Dateien speichern Bilddaten in einem Format, das für den Stanford-MPEG-Codec erforderlich ist.

HINWEIS: Die Befehlszeilenprogramme yuvsplittoppm und ppmtoyuvsplit sind Teil des Unix-basierten Grafikpakets netpbm.