BMC PSL statement-main()

main()

function main() {
BLOCK
}

Defines BLOCK as the entry point of a PSL program that begins with one or more function definitions.