ऑल्ट-एर्गो - क्लाउड में ऑनलाइन

कार्यक्रम:

नाम

Alt-Ergo - प्रोग्राम सत्यापन के लिए समर्पित एक स्वचालित प्रमेय कहावत

SYNOPSIS

ऑल्ट-एर्गो [ विकल्पों ] पट्टिका

वर्णन

ऑल्ट-एर्गो एक स्वचालित प्रमेय कहावत है. यह इनपुट के रूप में एक मनमाना बहुरूपी और लेता है
बहु-क्रमबद्ध प्रथम-क्रम सूत्र लिखा गया वाक्यविन्यास की तरह क्यों है।

विकल्प

-h मदद। आपको कमांड लाइन विकल्पों की पूरी सूची देगा।

उदाहरण

पूर्णांक अनुक्रमणिका के साथ कार्यात्मक सरणियों का एक सिद्धांत। यह सिद्धांत एक अंतर्निहित प्रकार प्रदान करता है
('ए,'बी) फ़रेरे और सरणियों में हेरफेर के लिए एक अंतर्निहित वाक्यविन्यास।

उदाहरण के लिए, एक अमूर्त डेटाटाइप tau और एक कार्यात्मक सरणी t प्रकार (int,
ताऊ) फ़ार्रे को इस प्रकार घोषित किया गया:

ताऊ टाइप करें

तर्क t: (int, tau) फ़रे

भाव:

t[i] सूचकांक i पर t में संग्रहीत मान को दर्शाता है

t[i1<-v1,...,in<-vn] एक सरणी को दर्शाता है जो प्रत्येक के लिए t के समान मान संग्रहीत करता है
संभवतः i1,...,in को छोड़कर सूचकांक, जहां यह मान v1,...,vn संग्रहीत करता है। यह अभिव्यक्ति
((t[i1<-v1])[i2<-v2])...[in<-vn] के बराबर है।

उदाहरण।

टी[0<-v][1<-w]

टी[0<-वी, 1<-डब्ल्यू]

टी[0<-वी, 1<-डब्ल्यू][1]

गणना प्रकारों का एक सिद्धांत.

उदाहरण के लिए कंस्ट्रक्टर ए, बी, सी के साथ एक गणना प्रकार टी को निम्नानुसार परिभाषित किया गया है
:

टाइप टी = ए | बी | सी

जिसका अर्थ है कि प्रकार t के सभी मान या तो A, B या C के बराबर हैं। और वह सब
ये कंस्ट्रक्टर अलग हैं।

बहुरूपी अभिलेखों का एक सिद्धांत.

उदाहरण के लिए, एक बहुरूपी रिकॉर्ड प्रकार 'at, जिसमें 'a और' प्रकार के दो लेबल a और b हैं
int को क्रमशः इस प्रकार परिभाषित किया गया है:

टाइप करें 'at = { a : 'a; बी : पूर्णांक }

भाव { a = 4; b = 5 } और { r with b = 3} रिकॉर्ड को दर्शाते हैं, जबकि बिंदु
लेबल तक पहुँचने के लिए नोटेशन ra का उपयोग किया जाता है।

Alt-Ergo (v. >= 0.95) उपयोगकर्ता को सिंटैक्स का उपयोग करके शब्दों के प्रकार को बाध्य करने की अनुमति देता है :
. नीचे दिया गया उदाहरण इस नई सुविधा के उपयोग को दर्शाता है।

'एक सूची' टाइप करें

तर्क शून्य : 'बी सूची

तर्क f : 'c सूची -> int

लक्ष्य g1: f(nil) = f(nil) (* मान्य नहीं है क्योंकि nil के दो उदाहरण हो सकते हैं
अलग - अलग प्रकार *)

लक्ष्य g2: f(शून्य:'d सूची) = f(शून्य:'d सूची) (* मान्य *)

वातावरण चर

एर्गोलिब
Alt-Ergo लाइब्रेरी के लिए वैकल्पिक पथ

लेखक

सिल्वेन कोंचोन <[ईमेल संरक्षित]> और एवलिन कॉन्टेजेन <[ईमेल संरक्षित]>

onworks.net सेवाओं का उपयोग करके ऑनलाइन ऑल्ट-एर्गो का उपयोग करें