ACSL چیه؟ این کلمه مخفف عبارت ANSI/ISO C Specification Language است؛ یک زبان مشخصات
رفتاری برای برنامه های نوشته شده به زبان C. طراحی ACSL از JML الهام گرفته شده.
ACSL برای نوشتن مشخصه هایی که یک قرارداد تابع رو میسازن، ساخته شده. ACSL میتونه دامنه وسیعی از functional property ها رو اعلام کنه.
مفهوم اساسی در ACSL "قرارداد تابع" یا Function contract هست. قرارداد تابع یعنی چی؟ توضیح واضح و دقیق از مشکلی که تابع حل میکنه رو میگیم قرارداد تابع. مثلا تابع isprime(n) مقدار true رو برمیگردونه اگر n عدد اول (Prime) باشه و در غیر اینصورت مقدار false را برمیگردونه. نکته مهم در مورد قرارداد تابع اینه که باید برای هر پارامتر گفته بشه که برای چه کاریه.
ACSL یک زبان Formal محسوب میشه. این یعنی مشخصات یا Specification نوشته شده به زبان ACSL به صورت خودکار توسط برنامه های Helper قابل فهمه، همونطور که یک کامپایلر زبان برنامه نویسی رو می فهمه. فرق کامنت با ACSL اینه که کامنت داده ای informal محسوب میشه و فقط توسط انسان قابل فهمه.
ACSL به ما امکان نوشتن قراردادهایی از محدوده سطح پایین (مثل: "این تابع انتظار دریافت یه valid pointer به int رو داره") تا سطح بالا (مثل: "این تابع انتظار یک لیست پیوندی غیرتهی از int ها رو داره و بزرگترین مقدار بین این int ها را برمیگردونه.") رو ارائه میده.
Assertion: یک property که هر وقت اجرا به یک نقطه از برنامه رسید باید verify بشه. مثال زیر رو در نظر بگیرید:
/*@ requires n >= 0 && n < 100; */ int f (int n) { int tmp = 100 - n; //@assert tmp > 0; //@assert tmp < 100; return tmp; }
Assertion اول به صورت اتوماتیک توسط بسیاری از آنالیزگرهای کد verify میشه اما برای دومی این اتفاق نمیفته و ممکنه یک آنالیزگر پیشنهاد این pre-condition رو بده: n>0
Pre-condition: شرطی است از نوع نیازمندی های آغازین و مربوط به قبل از اجرای کد است. مثلا در زیر یک نمونه از Pre-condition رو مشاهده میکنیم (pre-condition ها با کلمه کلیدی requires نوشته میشن):
/*@ requires n >= 0 */
Post-condition: یک شرط است در مورد پایان اجرای تابع و مقدار return شده. در زیر یک post-condition رو مشاهده میکنید (post-condition ها با کلمه کلیدی ensures نوشته میشن):
/* @ ensures \result >= x && \result >= y; */
میتونید برای کسب اطلاعات بیشتر در مورد ACSL این پی دی اف ها رو چک کنید:
https://frama-c.com/download/acsl-tutorial.pdf
https://frama-c.com/download/acsl.pdf
https://frama-c.com/download/frama-c-acsl-implementation.pdf
