How to use function's attribute?

Feb 24, 2013 at 11:07 AM
Hi,

I noticed that some functions are declared with the attribute "inline" in DafnyPrelude.bpl, shown as below:
type HeapType = <alpha>[ref,Field alpha]alpha;
function {:inline true} read<alpha>(H:HeapType, r:ref, f:Field alpha): alpha { H[r, f] }
function {:inline true} update<alpha>(H:HeapType, r:ref, f:Field alpha, v:alpha): HeapType { H[r,f := v] }
Could you explain the usage of "inline". Is there any other attributes, in addition to "inline". I did not find how to use function attributes in "This is Boogie 2".

Thanks
Yuyan
Feb 26, 2013 at 2:57 AM
Inline functions are a lot like a placeholder. Once you define an inline function, using the 'inline' keyword, whenever you call that function the compiler will replace the function call with the actual code from the function.

Nightrise
Feb 26, 2013 at 11:14 AM
OK.

Thanks
Yuyan