Persistent Ghosts परिचय: पिछले अध्यायों में, हमने उन storage values और मात्राओं को रिकॉर्ड करने के लिए ghost variables (hooks के माध्यम से) का उपयोग किया था जिन्हें smart contracts में स्पष्ट रूप से ट्रैक नहीं किया गया था — उदाहरण के लिए, ...

ERC-721 के लिए Invariants का परिचय पिछले अध्यायों में, हमने जाना कि CVL invariants कैसे काम करते हैं: ऐसे गुण जिन्हें पूरे कॉन्ट्रैक्ट निष्पादन के दौरान कायम रहना चाहिए। Invariants ... में पूर्व-शर्तों के रूप में कार्य कर सकते हैं...

Rules में Ghost Values को Constrain करना पिछले अध्याय में, हमने सीखा कि कैसे ghost variables जानकारी को hooks से rules में प्रवाहित होने देते हैं। हमने यह भी सीखा कि: Verification की शुरुआत में...

ERC-721 के लिए आंशिक रूप से पैरामेट्रिक नियमों का परिचय। यह अध्याय OpenZeppelin के ERC-721 CVL स्पेसिफिकेशन के कोड वॉकथ्रू का अंतिम भाग (5/5) है, जो निम्नलिखित को औपचारिक रूप से सत्यापित करता है...

ERC-721 के लिए Transfer और Approval नियम परिचय यह अध्याय OpenZeppelin के ERC-721 CVL specification के हमारे code walkthrough के तीसरे भाग (3/5) के रूप में जारी है और token transfer पर केंद्रित है...

Preserved Block और Invariant Verification में इसकी भूमिका Invariant एक ऐसी विशेषता है जिसे स्मार्ट कॉन्ट्रैक्ट के डिप्लॉय होने के बाद और इसके पूरे निष्पादन के दौरान हमेशा सत्य रहना चाहिए। पहली नज़र में,...

Rules और Invariants में “requireInvariant" का उपयोग: अब तक, हमने या तो विशिष्ट व्यवहारों को सत्यापित करने के लिए एक rule लिखा है या उन गुणों को सत्यापित करने के लिए एक invariant लिखा है जो पूरे... के दौरान हमेशा सत्य रहने चाहिए।

ERC-721 के लिए Mint और Burn के नियम परिचय ERC-721 non-fungible tokens के लिए Ethereum मानक है, जिसका व्यापक रूप से डिजिटल संपत्ति का प्रतिनिधित्व करने के लिए उपयोग किया जाता है। संपत्ति के किसी भी रूप की तरह, यह आपूर्ति के इर्द-गिर्द घूमता है...

CVL में msg.sender और msg.value की टेस्टिंग परिचय इस अध्याय में, हम CVL में उस वेरिएबल का परिचय देते हैं, जो हमें उन फंक्शन्स के लिए नियम बनाने में सक्षम बनाता है जो , , और ... में अन्य ग्लोबल वेरिएबल्स पर निर्भर करते हैं।

Method Properties का परिचय परिचय पिछले अध्याय में, हमने parametric rules के बारे में सीखा था, जो हमें उन properties को formally verify करने की अनुमति देते हैं जिनके हमेशा सत्य रहने की उम्मीद की जाती है, भले ही कोई भी...

Formal Verification का परिचय Formal verification गणितीय रूप से यह सिद्ध करने की प्रक्रिया है कि कोई प्रोग्राम किसी specification का पालन करता है। यह लेख वैचारिक रूप से इस बात का परिचय देता है कि formal verification कैसे...

Certora CVL में Spec File को समझना। पिछले अध्याय में, हमने देखा कि Certora Prover का उपयोग करके formal verification करने के लिए, हमें Prover को निम्नलिखित प्रमुख चीजें प्रदान करने की आवश्यकता होती है: Smart...