نوشته های یاسر آرامش

7 دلیل برای بهتر بودن Solana از Ethereum (تا قبل از ظهور کامل Ethereum 2.0)

یاسر آرامش — Thu, 13 Jan 2022 03:07:55 +0330

1. تراکنش بر ثانیه (Transactions Per Second)سولانا به طوری اساسی در میزان TPS از اتریوم جلوتره. شبکه ی اتریوم به میزان سنگینی شلوغه و حدود 10 الی 15 ثانیه طول میکشه تا یک تراکنش پردازش بشه (یک بلوک ماین بشه) و در هر ثانیه 15 تا 45 تراکنش قابل انجامه. اونطرف سولانا در 400 میلی ثانیه یک بلوک رو ماین میکنه. سولانا میتونه 50 هزار TPS رو هندل کنه و توانایی ارتقا تا 65 هزار TPS رو هم داره. البته این مزیت تا ابد باقی نمیمونه. در 2022 به مرور Ethereum آپگرید میشه در قالب فاز های مختلف و با ظهور کامل Ethereum 2.0، پیش بینی میشه 100 هزار TPS قابل انجام باشه.2. هزینه ی هر تراکنشهر تراکنش یه هزینه (fee) داره که تو زبان رمزارزها بهش gas fee گفته میشه و به کامپیوترهایی که تراکنش ها رو پردازش میکنن پرداخت میشه. طبق هر پلتفرم بلاک چین (بیت کوین، اتریوم، سولانا) این هزینه متفاوت هست. سولانا به میزان شگفت انگیزی fee کمتری نسبت به اتریوم داره (به طور متوسط 0.00025 دلار هست fee سولانا). با ظهور کامل اتریوم 2.0، fee اتریوم هم مثل سولانا نزدیک به صفر میشه. 3. سولانا مشکل Mempool رو ندارهیک Mempool، محیط انتظاری هست که یک تراکنش پردازش شده در انتظار قرار گیری روی بلاک چین هست. در سولانا تراکنش ها تقریبا درجا روی بلاک چین قرار میگیرن. روی اتریوم، تقریبا 4 دقیقه طول میکشه که تراکنش Verify بشه و روی بلاک چین قرار بگیره.4. سولانا راحت تر برنامه نویسی میشهاتریوم بر پایه نرم افزار Solidity که برای اترویم طراحی شده کار میکنه اما کدهای سولانا با Rust نوشته میشه. Rust برای ساخت بازی ها و بلاک چین استفاده میشه. مبتنی بر Rust بودن باعث ساده تر شدن گسترش اکوسیستم سولانا شده.5. اکوسیستم سولانا گسترش سریعتری دارهبا اینکه همچنان اتریوم الویت اول انتخاب شدن برای ساخت و میزبانی برنامه های غیرمتمرکز (DApps) و پیاده سازی قراردادهای هوشمند (Smart contracts) رو داره با چالش های هزینه و سرعت مواجهه. سولانا فعلا این چالش ها رو نداره و استفاده ازش به صورت تصاعدی تو حوزه DApps در حال گسترشه.6. سولانا از پهنای باند کمتری استفاده میکنه سولانا از پروتکلی به نام Turbine استفاده میکنه که پهنای باند مصرفی رو نسبت به اتریوم به شدت کاهش میده.7. سولانا برای محیط زیست بهترهسولانا بر خلاف اتریوم که از الگوریتم اجماع Proof of Work استفاده میکنه، دو الگوریتم Proof of Stake و Proof of History رو به کار گرفته که 99.9 درصد مصرف انرژی بهینه تری دارن.

کرونا و محیط زیست؛ این هشداری دیگر از طبیعت است...

یاسر آرامش — Tue, 26 May 2020 19:01:54 +0430

خانم Inger Anderson، مدیر برنامه محیط زیست سازمان مللمدیر بخش محیط زیست سازمان ملل، خانم Inger Anderson میگوید طبیعت با کروناویروس جدید و بحران تغییرات آب و هوایی (Climate Crisis) به ما پیام میدهد.اندرسون گفت انسان ها فشار زیادی بر روی دنیای طبیعی وارد کردند که عواقب مضری داشت، و هشدار داد شکست خوردن در مراقبت از سیاره، شکست خوردن در مراقبت از خود ما انسان هاست.همچنین دانشمندان پیشرو گفته اند که شیوع Covid-19 یک "شلیک هشدار واضح" است. آنها میگویند تقریبا همیشه به دلیل رفتار انسانی بیماری ها از حیوانات به انسان ها سرایت کرده.برای جلوگیری از شیوع های بعدی، متخصصین میگویند هم گرمایش جهانی و هم از بین بردن طبیعت برای کشاورزی، معدن کاوی و خانه سازی باید متوقف بشوند چون هر دو طبیعت وحشی را با ما در ارتباط قرار میدهند.متخصصین همچنین به مقامات اصرار کردند تا بر کار بازارهای حیوانات زنده و تجارت غیرمجاز جهانی حیوانات پایان بدهند.اندرسون گفت الویت اضطراری حال حاضر محافظت از مردم در مقابل کروناویروس و جلوگیری از شیوع آن است اما پاسخ بلند مدت ما باید مقابله با از بین رفتن زیستگاه ها و تنوع زیستی باشد.اندرسون افزود: "هیچ وقت در گذشته به این تعداد فرصت برای عوامل بیماری زا وجود نداشته تا از حیوانات اهلی و وحشی به انسان ها سرایت بکنند". به گفته او 75 درصد بیماری های مسری شایع از حیات وحش می آیند.او همچنین اشاره ای به آتش سوزی های استرالیا، شکسته شدن رکوردهای گرمایش زمین و بدترین حمله ملخ ها در 70 سال گذشته به کنیا کرد و گفت طبیعت در حال پیام دادن به ما است.شیوع بیماری های مسری میان انسان ها در حال افزایش است و در سال های اخیر ما ابولا، آنفولانزای پرندگان، مِرس، سارس، تب دره ریفت، ویروس نیل غربی و زیکا رو داشتیم که همه از حیوانات به انسان ها منتقل شدند.پروفسور اندرو کانینگهام میگوید: "وضعیت اضطراری و شیوع کووید-19 نه تنها قابل پیش بینی بود، بلکه به گونه ای حتی پیش بینی شده بود." یک تحقیق در سال 2007 که در مورد شیوع بیماری Sars در سال های 2002 و 2003 بود منتشر شده بود که نتیجه گیری کرده بود: "وجود یک ذخیره عظیم از ویروس های مشابه Sars-Cov در خفاش های نعل بینی همراه با فرهنگ خوردن پستانداران غیربومی (exotic) در جنوب چین یک بمب ساعتی است."کانینگهام گفت دیگر بیماری های با منشا حیات وحش نرخ مرگ و میر بالاتری داشتند، مانند اِبولا (50 درصد) و ویروس نیپا (60-75 درصد) که از طریق خفاش ها در جنوب آسیا به انسان سرایت کردند. "با اینکه ممکن است شما این فکر را نکنید، اما ما احتمالا در زمینه Covid-19 کمی خوش شانس بودیم."او در ادامه گفت ما باید Covid-19 را هشداری جدی تلقی کنیم و گفت حیوانات در مسافت های طولانی حمل میشوند و با هم در قفس ها قرار میگیرند؛ آنها استرس تجربه میکنند و عوامل بیماری زای خود را بیرون میریزند. با تعداد افراد زیاد در بازار و ارتباط آنها با مایع بدن این حیوانات بهترین موقعیت برای شیوع ایجاد میشود.چین موقتا این بازارها را تعطیل کرده است اما کانینگهام میگوید این مسئله باید دائمی باشد. او همچنیی وجود چنین بازهایی در بعضی مناطق آفریقا و بسیاری از کشورهای آسیایی اشاره کرد.آقای Aaron Bernstein از دانشگاه سلامت عمومی هاروارد میگوید از بردن مناطق طبیعی حیات وحش را به سمت زندگی کردن در نزدکی ما هدایت میکند و تغییرات اقلیمی نیز حیوانات را مجبور به جا یه جایی میکند.او گفت: "ما سارس، مرس، کووید-19 و HIV را داشتیم. ما باید ببینیم طبیعت چه چیزی به ما میگوید. ما باید متوجه شویم که در حال بازی با آتش هستیم. جدایی سیاست های سلامت و محیط زیست یک تصور خطرناک است. سلامت ما به طور کامل وابسته شرایط جوی و دیگر ارگانیسم هایی است که این سیاره را با آنها شریک هستیم".آقای John Scanlon، دبیر کل مجمع CITES میگوید: "تجارت میلیارد دلاری غیرقانونی حیات وحش بخش دیگری از مشکل است. کشورهای وارد کننده باید قوانین جدیدی وضع کنند تا وارد کنندگان حیات وحش ملزوم به اثبات به دست آوردن قانونی حیوان طبق قوانین ملی کشور مبدا باشند. او همچنین گفت: "اگر بتوانیم مقابله سخت با مجرمین حیات وحش سازمان یافته بین المللی را همزمان با ایجاد فرصت های جدید برای جوامع محلی انجام دهیم، سپس شاهد شکوفا شدن تنوع زیستی، اکوسیستم ها و جوامع خواهیم بود."محموله هزاران Pangolin یخ زده غیرمجاز کشف شده توسط پلیس (صحنه پیش از سوزانده شدن)بحران Covid-19 میتونه یک فرصت برای تغییر ارائه بده، اما کانینگهاک معتقد نیست که از این فرصت استفاده بشه: “ من فکر میکردم بعد از Sars که یک هشدار بیدار کننده بزرگ بود اوضاع عوض بشود. Sars بزرگترین تاثیر اقتصادی را از بین بیماری‌های نوظهور داشت".کانیگهام گفت: “همه برای تغییر آماده بودند. اما به خاطر اقدامات کنترلی ضعیف کمرنگ شد. بعد آرامش از راه رسید و کارها مثل سابق ادامه پیدا کرد. ما نمیتوانیم مثل سابق باشیم."منبع: The Gurdian

آشنایی با Frama-C، ابزاری برای تست کد C

یاسر آرامش — Fri, 14 Feb 2020 18:14:47 +0330

Frama-C یک پلتفرم اختصاصی و قابل گسترش برای آنالیز سورس کد زبان C است.Frama-C یک سری تکنیک های آنالیز ایستا را در یک فریمورک گرد هم آورده. این رویکرد Frama-C باعث شده که آنالیزگرها از نتایج از پیش محاسبه شده یکدیگر استفاده کنند و به لطف این رویکرد ابزارهای پیچیده ای همچون آنالیز وابستگی و Slicer در Frama-C ارائه میشوند.این ابزار برای سیستم عامل های Mac و لینوکس ارائه شده و از طریق ابزار Cygwin و یا WIndows Subsystem for Linux در ویندوز نیز قابل استفاده است. توضیحات اینجانب بر اساس اجرای Frama-C بر روی Ubuntu 19.10 Eoan Ermine است اما قابل اجرا بر روی نسخه های قبل تر نیز میباشد.پلاگینی برای افزودن پشتیبانی از ++CFrama-Clang یک پلاگین است که Frama-C را قادر میکند تا برنامه های C++ را به عنوان ورودی بگیرد.این پلاگین همانطور که از نامش پیداست، مبتنی بر clang compiler است.آپدیت کردن پکیج های سیستم عامل:دستورات زیر به ترتیب وارد میشوند.sudo apt-get update sudo apt-get upgradeدستور اول برای گرفتن اطلاعات پکیج ها از منابع مشخص شده در فایل /etc/apt/sources.list و دستور دوم برای نصب آپدیت پکیج های از پیش نصب شده روی سیستم است.نصب opam و Frama-Cبرای نصب frama-c روش opam انتخاب شده. Opam یک Package Manager برای OCamle است. برای نصب opam از دستور زیر استفاده میشود:sudo apt-get install opamFrama-c یک سری dependency های غیر OCamle ای از جمله Gtk و GMP دارد. در بسیاری از سیستم ها opam میتواند این وابستگی های خارجی را با پلاگین depext فراهم کند. برای استفاده از depext اینگونه عمل میکنیم:opam install depext opam depext frama-cاگر سیستم توسط depext پشتیبانی نشود باید Gtk, GtkSourceView, GnomeCanvas و GMP جداگانه نصب شوند.بعد از نصب وابستگی ها، خود frama-c با دستور زیر نصب میشود:opam install frama-c اجرای رابط کاربری گرافیکی Frama-Cبا وارد کردن دستور frama-c-gui در ترمینال میتوان رابط کاربری گرافیکی یا gui این برنامه را اجرا کرد.در زمان اجرای frama-c-gui ممکن است با خطای زیر مواجه شوید:Gtk-Message: Failed to load module "canberra-gtk-moduleخطای بالا به احتمال فراوان با دستور زیر رفع میشود:sudo apt-get install libcanberra-gtk*ممکن است حین اجرای دستور بالا با خطایی بدین شکل مواجه شوید:E: Could not get lock /var/lib/dpkg/lock - frontend – open (11: Resource temporarily unavailable)در این صورت با دستور زیر process ها را بسته و دوباره کد نصب libcanberra-gtk را وارد میکنید:sudo killall apt apt-getاگر دوباره ارور قبلی را دریافت کردید ری استارت کردن را امتحان کنید.در صورتی که باز هم این مشکل را داشتید طبق این آموزش پیش بروید (و اگر سوالی داشتید در قسمت نظرات بپرسید).شروع کار با Frama-C و استفاده از Call Graphبرای افزودن پروژه (سورس برنامه) از تب Project گزینه New Project را فشرده و فایل سورس کد را انتخاب میکنیم.این سورس کدی است که در این آزمون استفاده شده (محاسبه بزرگترین مقسوم علیه مشترک و کوچکترین مضرب مشترک):#include long gcd(long, long); int unused; int test; int main() { long x, y, hcf, lcm; printf("Enter two integers:\n"); scanf("%ld%ld", &x, &y); hcf = gcd(x, y); lcm = (x*y)/hcf; printf("Greatest common divisor of %ld and %ld = %ld\n", x, y, hcf); printf("Least common multiple of %ld and %ld = %ld\n", x, y, lcm); return 0; } long gcd(long x, long y) { if (x == 0) { return y; } while (y != 0) { if (x > y) { x = x - y; } else { y = y - x; } } return x; }یکی از ساده ترین کاربردهای Frama-C استخراج Call Graph برنامه است که میتوانیم از طریق آن فراخوانی های توابع را مشاهده کنیم. برای مشاهده Call graph کل برنامه، گزینه Show entire callgraph از تب Analyses و برای مشاهده callgraph تابع انتخاب شده، گزینه show callgraph from current function را انتخاب میکنیم.Call graphلیست آنالیزهای Frama-Cلیست کامل آنالیزهای Frama-C که از طریق گزینه Analyses در تب Analyses در دسترس هستند در تصویر زیر قابل مشاهده است:Frama-C Analysesآنالیز Usersاین آنالیز توابع فراخوانی شده، printf ها و scanf های یک تابع را نشان میدهد. نتیجه را در تب کنسول پایینِ برنامه میتوانید مشاهده کنید.Frama-C Users آنالیز inoutورودی ها و خروجی های تابع را آنالیز کرده و از EVA نیز استفاده میکند. EVA هم یک سری Assertion به سورس کد برنامه می افزاید (دایره های نارنجی در عکس پایین). با EVA در ادامه پست آشنا میشوید.inout and EVA analyses آنالیز PDGگراف وابستگی برنامه یا Program Dependence Graph، گرافی است که وابستگی های کنترلی و داده ای statement ها به یکدیگر را نشان میدهد. برای استخراج PDG سورس کد در قالب فایل dotو تبدیل آن به pdf بدین صورت عمل میکنیم:1: در مسیری که سورس کد وجود دارد کلیک راست کرده و open in terminal را میزنیم.2: دستورهای زیر را وارد میکنیم. به جای file.c نام فایل خود را تایپ میکنیم.در دستور دوم به جای pdg در pdg.pdf، نام دلخواه خود را تعیین میکنیم.frama-c -pdg -pdg-dot graph -pdg-print file.c > pdg.dot dot -Tpdf graph.main.dot > pdg.pdfPDGآنالیز Postdominatorsاین آنالیز با scanf و printf مشکل دارد. برای استفاده از این آنالیز یک راه حل، ورودی را دستی وارد کردن ( استفاده نکردن از scanf ) و استفاده از return به جای printf است، یک راه دیگر کامنت کردن دستورات scanf و printf است.به جای file.c نام فایل سورس کد را وارد میکنیم. برای نمایش postdominators هر تابع در قالب pdf از دستورات دوم و سوم استفاده شده. دستور دوم postdominators تابع gcd برنامه نمونه را فراهم میکند و دستور سوم postdominators تابع main را.frama-c file.c -dot-postdom main dot -Tpdf main.gcd.dot > gcdPostdominators.pff dot -Tpdf main.main.dot > mainPostdominators.pdfآنالیز WPپلاگین WP یک پیاده سازی فوق العاده از Weakest Precondition calculus برای برنامه های annotated به زبان C است. یکی از مزیت های WP این هست که مثل Jessie کد C را به Why کامپایل نمیکند و به همین خاطر مشکلی نیست که نتایج WP با تکنیک های دیگری همچون Eva plug-in ترکیب شود.به طور پیشفرض، WP Plug-in هیچ proof obligation ای مبنی بر وجود نداشتن runtime errors (خطاهای زمان اجرا) تولید نمیکند. وجود نداشتن خطاهای زمان اجرا میتواند توسط تکنیک های دیگری (برای مثال Eva plug-in) یا با تولید تمام annotation های ضروری توسط RTE Plug-in ثابت شود.پلاگین WP در Frama-c از پلتفرم Why3 برای اجرای external prover ها استفاده میکند. دلیل استفاده از external prover ها اثبات یا verify کردن ACSL annotations است. پلتفرم Why3 و Alt-Ergo prover به صورت اتوماتیک توسط opam موقع نصب frama-c نصب میشوند.به جز Alt-Ergo این prover ها نیز در سایت Frama-C به عنوان Prover های پیشنهادی و بهینه معرفی شده اند: CVC4 و Z3Z3 ارائه شده توسط Microsoft Research و تحت لیسانس MIT است. Z3 برای بسیاری زبان های برنامه نویسی از جمله Python, Java, C++, .NET و ...Binding دارد. Why3 بعد از نصب باید Config )پیکربندی) بشود تا برای Frama-C/WP در دسترس قرار گیرد. این پیکربندی با دستور زیر انجام میشود:Why3 config -detectWP هم از طریق GUI و هم batch mode (Terminal) قابل دسترسی است. از دستور frama-c -wp gcdlcm.c برای اجرای wp در batch mode استفاده کردیم و نتیجه زیر حاصل شد. (gcdlcm.c نام برنامه مورد نظر است)WP Pluginاگر با خطای زیر مواجه شدید اول با اجرای دستور opam install alt-ergo altgr-ergo از نصب alt-ergo اطمینان حاصل کنید، و بعد با دستور Why3 config -detect که قبل تر نیز اشاره کردیم پیکربندی را انجام دهید:User Error: No prover in /home/yourusername/.why3.conf corresponds to "alt-ergo"در این سایت میتوانید alt-ergo را امتحان کنید. برش بندی یا Slicingعبارت است از عمل برش بندی برنامه بر اساس یک معیار برش بندی (Slicing Criterion). وقتی برش بندی انجام شود تمام کدهایی که بر روی معیار برش بندی تاثیر مستقیم یا غیرمستقیم دارند در یک برش قرار میگیرند. به جای file.c نام برنامه خود و به جای variable متغیری که میخواهید به عنوان معیار برش تعیین شود را تایپ کنید.frama-c -slice-wr variable file.c > slice.txtاین پلاگین از نتایج پلاگین Value analysis و محاسبات وابستگی های تابع استفاده میکند.آنالیز Metricsاین آنالیز برای ما موارد زیر را محاسبه میکند:• McCabe's cyclomatic complexity• Halstead complexity • Value analysis coverage estimateکد اول آنالیز metrics را انجام داده و در ترمینال نتیجه را نشان میدهد، کد دوم آنالیز را اجرا میکند اما نتیجه را در یک فایل txt ذخیره میکند:frama-c file.c -metrics frama-c file.c -metrics > metrics.txtبرای استفاده از گزینه -metrics-value-cover این پلاگین به نتایج Value analysis نیاز دارد.آنالیز EVAEVA مخفف Evolved Value Analysis است.پلاگین EVA به صورت خودکار variation domain های متغیرهای برنامه را محاسبه میکند و assertion های لازم را اضافه میکند.این پلاگین هم در GUI و هم در batch mode قابل استفاده است.دستور اجرای EVA در ترمینال:frama-c -eva file1.c EVA Plug-inدستور اجرای همزمان EVA روی دو فایل:frama-c -eva file1.c file2.cنتایج EVA توسط بسیاری از پلاگین ها استفاده میشود.محدودیت ها: فراخوانی های بازگشتی در حال حاظر پشتیبانی نمیشوند و فقط کد Sequential میتواند آنالیز شود.آنالیز Rte:annotation پلاگینی است برای ساخت خطاهای زمان اجرای معمول، overflow های عملیات های unsigned integer و function contracts inlining در محل های فراخوانی (call sites)این پلاگین نیز همانند بسیاری از پلاگین ها هم از طریق GUI و هم batch mode قابل استفاده است.نتیجه استفاده در gui با فعال بودن تمام گزینه ها:RTE Plug-inاستفاده معمولی از Rte:frama-c -rte file.cبرای تولید همه ی annotation های همه توابع، از جمله function contracts inlining از دستور زیر استفاده میشود:frama-c -rte -rte-unsigned-ov file.cبرای اینکه annotation های یک یا چند تابع مشخص از برنامه را تولید کنیم از کد زیر استفاده میکنیم:frama-c -rte -rte-select function1,function 2 file.cیکی از محدودیت های RTE این است که هیچ contract ای در محل های فراخوانی توابعی که از طریق pointer صدا زده شده اند تولید نمیشود.آنالیز Sparecodeاین پلاگین کار حذف کدهای غیرضروری در برنامه را انجام میدهد. Statement ها و توابعی که برای محاسبه نتیجه برنامه لازم نیستند توسط کد زیر حذف میشوند:Frama-c -sparecode-analysis file.cکد زیر هم متغیرهای سراسری و type های تعریف شده اما استفاده نشده را حذف میکند و کد جدید (بدون آن موارد استفاده نشده را) در یک فایل txt ذخیره میکند:Frama-c -sparecode-rm-unused-globals file.c > sparecode.txtکد برنامه را تغییر دادیم و دو دستور غیرضروری و بدون کاربرد را اضافه کردیم. یک متغیر سراسری تعریف کردیم به نام test و در تابع gcd مقدار y را در متغیر test قرار دادیم. برای اجرای این آنالیز از طریق gui گزینه Analyses را از تب Analyses انتخاب کرده و سپس از لیست گزینه sparecode را انتخاب میکنیم.

آشنایی با ACSL

یاسر آرامش — Fri, 14 Feb 2020 16:15:00 +0330

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>0Pre-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.pdfhttps://frama-c.com/download/acsl.pdfhttps://frama-c.com/download/frama-c-acsl-implementation.pdf