Cランタイムを理解する
Cランタイム(CRT)は、プログラムが実行されるために必要な初期化ルーチン、ライブラリのサポートコード、システムコールのラッパなどをまとめた仕組みです。本記事では、CRTのスタートアップオブジェクトに含まれる crt0.o、crt1.o、crti.o、crtn.o などのファイルがどのような役割を持ち、なぜ存在するのか、そしてC(およびC++)プログラムがスムーズに動作するためにどのように連携しているのかを解説します。
Cランタイム(CRT)は、プログラムが実行されるために必要な初期化ルーチン、ライブラリのサポートコード、システムコールのラッパなどをまとめた仕組みです。本記事では、CRTのスタートアップオブジェクトに含まれる crt0.o、crt1.o、crti.o、crtn.o などのファイルがどのような役割を持ち、なぜ存在するのか、そしてC(およびC++)プログラムがスムーズに動作するためにどのように連携しているのかを解説します。
このブログでは、「計算機科学における論理」という本で説明されている命題論理の基礎を概説します。
レスリー・ランポートによる「TLA+入門」コースのコンスペクトの第2部。
レスリー・ランポートによる「TLA+入門」コースのコンスペクトの第1部。
このブログでは、スモールステップとビッグステップのセマンティクス、その違い、コンピュータプログラムの分析への応用について概説します。
このブログでは、線形時相論理および計算木論理を探求し、それらをどのようにスマートコントラクトの検証に使用できるかを説明します。
このブログでは、プログラム検証の文脈で形式的仕様の利点を探ります。