זוהי הפקודה why-dp שניתן להפעיל בספק האירוח החינמי של OnWorks באמצעות אחת מתחנות העבודה המקוונות המרובות שלנו, כגון Ubuntu Online, Fedora Online, אמולטור מקוון של Windows או אמולטור מקוון של MAC OS
תָכְנִית:
שֵׁם
למה - כלי אימות רב שפות מרובה מוכיחים
תַקצִיר
למה [ אפשרויות ] קבצים
תיאור
למה הוא כלי אימות. זה לוקח תוכניות מוערות כקלט (בתחביר ML או C) ו
מפלט תנאי אימות עבור מספר עוזרי הוכחה (Coq, PVS, HOL Light, Mizar)
ונהלי החלטה (haRVey, Simplify).
אפשרויות
-h עֶזרָה. ייתן לך את הרשימה המלאה של אפשרויות שורת הפקודה.
מחברים
Jean-Christophe פיליאטר <[מוגן בדוא"ל]>
השתמש ב- why-dp באינטרנט באמצעות שירותי onworks.net
